The Sierpinski Object in the Scott Realizability Topos
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 obj...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-08-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5416/pdf |
| _version_ | 1797268596677672960 |
|---|---|
| author | Tom de Jong Jaap van Oosten |
| author_facet | Tom de Jong Jaap van Oosten |
| author_sort | Tom de Jong |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:00Z |
| format | Article |
| id | doaj.art-e5f6d6fdfa7c4aa3974e1348b21bde6e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:00Z |
| publishDate | 2020-08-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-e5f6d6fdfa7c4aa3974e1348b21bde6e2024-03-08T10:31:24ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-08-01Volume 16, Issue 310.23638/LMCS-16(3:12)20205416The Sierpinski Object in the Scott Realizability ToposTom de JongJaap van OostenWe 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.https://lmcs.episciences.org/5416/pdfcomputer science - logic in computer sciencemathematics - logic68q05, 18b25 |
| spellingShingle | Tom de Jong Jaap van Oosten The Sierpinski Object in the Scott Realizability Topos Logical Methods in Computer Science computer science - logic in computer science mathematics - logic 68q05, 18b25 |
| title | The Sierpinski Object in the Scott Realizability Topos |
| title_full | The Sierpinski Object in the Scott Realizability Topos |
| title_fullStr | The Sierpinski Object in the Scott Realizability Topos |
| title_full_unstemmed | The Sierpinski Object in the Scott Realizability Topos |
| title_short | The Sierpinski Object in the Scott Realizability Topos |
| title_sort | sierpinski object in the scott realizability topos |
| topic | computer science - logic in computer science mathematics - logic 68q05, 18b25 |
| url | https://lmcs.episciences.org/5416/pdf |
| work_keys_str_mv | AT tomdejong thesierpinskiobjectinthescottrealizabilitytopos AT jaapvanoosten thesierpinskiobjectinthescottrealizabilitytopos AT tomdejong sierpinskiobjectinthescottrealizabilitytopos AT jaapvanoosten sierpinskiobjectinthescottrealizabilitytopos |