Every metric space is separable in function realizability
We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic d...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2019-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4651/pdf |
| _version_ | 1827322817875542016 |
|---|---|
| author | Andrej Bauer Andrew Swan |
| author_facet | Andrej Bauer Andrew Swan |
| author_sort | Andrej Bauer |
| collection | DOAJ |
| description | We first show that in the function realizability topos every metric space is
separable, and every object with decidable equality is countable. More
generally, working with synthetic topology, every $T_0$-space is separable and
every discrete space is countable. It follows that intuitionistic logic does
not show the existence of a non-separable metric space, or an uncountable set
with decidable equality, even if we assume principles that are validated by
function realizability, such as Dependent and Function choice, Markov's
principle, and Brouwer's continuity and fan principles. |
| first_indexed | 2024-04-25T01:34:50Z |
| format | Article |
| id | doaj.art-bdd0201a78524b9d90c1448e0883e2d3 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:50Z |
| publishDate | 2019-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-bdd0201a78524b9d90c1448e0883e2d32024-03-08T10:27:59ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742019-05-01Volume 15, Issue 210.23638/LMCS-15(2:14)20194651Every metric space is separable in function realizabilityAndrej BauerAndrew SwanWe first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles.https://lmcs.episciences.org/4651/pdfmathematics - logiccomputer science - logic in computer science54e35, 03f60, 03f55 |
| spellingShingle | Andrej Bauer Andrew Swan Every metric space is separable in function realizability Logical Methods in Computer Science mathematics - logic computer science - logic in computer science 54e35, 03f60, 03f55 |
| title | Every metric space is separable in function realizability |
| title_full | Every metric space is separable in function realizability |
| title_fullStr | Every metric space is separable in function realizability |
| title_full_unstemmed | Every metric space is separable in function realizability |
| title_short | Every metric space is separable in function realizability |
| title_sort | every metric space is separable in function realizability |
| topic | mathematics - logic computer science - logic in computer science 54e35, 03f60, 03f55 |
| url | https://lmcs.episciences.org/4651/pdf |
| work_keys_str_mv | AT andrejbauer everymetricspaceisseparableinfunctionrealizability AT andrewswan everymetricspaceisseparableinfunctionrealizability |