Andrej Bauer: All metric spaces are separable

Datum objave: 21. 3. 2018
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 22. 3. 2019, učilnica 3.07, Jadranska 21

Abstract: Are there any uncountable sets with decidable equality in constructive mathematics, or at least non-separable metric spaces? We put these questions to rest by showing that in the function realizability topos all metric spaces are separable, and consequently all sets with decidable equality countable. Therefore, intuitionistic logic does not show existence of non-separable metric spaces, even if we assume principles that are validated by function realizability, among which are the Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles.

This is joint work with Andrew Swan