Tom de Jong ; Jaap van Oosten - The Sierpinski Object in the Scott Realizability Topos

lmcs:5416 - Logical Methods in Computer Science, August 20, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:12)2020
The Sierpinski Object in the Scott Realizability ToposArticle

Authors: Tom de Jong ; Jaap van Oosten

    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.


    Volume: Volume 16, Issue 3
    Published on: August 20, 2020
    Accepted on: August 15, 2020
    Submitted on: May 1, 2019
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,68Q05, 18B25

    Consultation statistics

    This page has been seen 1722 times.
    This article's PDF has been downloaded 329 times.