一句话：研究 Scott 可实现性拓扑斯中的 Sierpinski 对象 Σ，刻画序离散对象、dominance 与同伦模型。
本文研究基于 Scott λ 演算图模型的可实现性拓扑斯中的 Sierpinski 对象 Σ。作者首先指出该拓扑斯中的 realizers 对象就是指数对象 Σ^N（N 为自然数对象），进而用与 Σ 的正交性定义序离散对象，证明它们构成反射子范畴，并说明高阶算术中许多基本对象均序离散。基于 Lietz 的工作，作者获得该拓扑斯内部逻辑的新结果；把 Σ 视为 dominance 后，显式构造 lift 函子并刻画 Σ-子对象，发现 Σ 对并不封闭。最后构造同伦模型，其中序离散对象恰为只有常路径的对象。
We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is the natural numbers object. We define order-discrete objects by orthogonality to $\Sigma$. We show that the order-discrete objects form a reflective subcategory of the topos, and that many fundamental objects in higher-type arithmetic are order-discrete. Building on work by Lietz, we give some new results regarding the internal logic of the topos. Then we consider $\Sigma$ as a dominance; we explicitly construct the lift functor and characterize $\Sigma$-subobjects. Contrary to our expectations the dominance $\Sigma$ is not closed under unions. In the last section we build a model for homotopy theory, where the order-discrete objects are exactly those objects which only have constant paths.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1904-13354,
title = {The Sierpinski Object in the Scott Realizability Topos},
author = {Tom de Jong and Jaap van Oosten},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 3},
year = {2020},
doi = {10.23638/lmcs-16(3:12)2020}
}