Every metric space is separable in function realizability

TL;DR

This paper demonstrates that within the framework of function realizability and synthetic topology, all metric spaces are separable and objects with decidable equality are countable, challenging certain classical assumptions.

Contribution

It shows that in the context of function realizability, all metric spaces are separable and objects with decidable equality are countable, under intuitionistic logic.

Findings

All metric spaces are separable in the function realizability topos.

Objects with decidable equality are countable.

Intuitionistic logic does not imply the existence of non-separable metric spaces.

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 $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.