Every metric space is separable in function realizability
| Authors |
|
|---|---|
| Publication date | 23-05-2019 |
| Journal | Logical Methods in Computer Science |
| Article number | 14 |
| Volume | Issue number | 15 | 2 |
| Number of pages | 7 |
| Organisations |
|
| Abstract | 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 T0T0-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. |
| Document type | Article |
| Language | English |
| Published at |
https://doi.org/10.23638/LMCS-15(2:14)2019
(Final published version)
|
| Published at |
https://arxiv.org/abs/1804.00427v6
(Final published version)
|
| Downloads |
1804.00427
(Final published version)
|
| Permalink to this page | |