Andrej Bauer: All metric spaces are separable

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.