Abstract
We study the Sierpinski object Σ in the realizability topos based on Scott's graph model of the λ-calculus. Our starting observation is that the object of realizers in this topos is the exponential ΣN, where N is the natural numbers object. We define order-discrete objects by orthogonality to Σ. 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 Σ as a dominance; we explicitly construct the lift functor and characterize Σ-subobjects. Contrary to our expectations the dominance Σ 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.
| Original language | English |
|---|---|
| Pages (from-to) | 1-16 |
| Journal | Logical Methods in Computer Science |
| Volume | 16 |
| Issue number | 3 |
| DOIs | |
| Publication status | Published - 20 Aug 2020 |
Keywords
- Computer Science
- Logic in Computer Science,Mathematics
- Logic,68Q05, 18B25
Fingerprint
Dive into the research topics of 'The Sierpinski Object in the Scott Realizability Topos'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver