How Unconstructive is the Cantor-Bernstein Theorem?

How Unconstructive is the Cantor-Bernstein Theorem? C´ecilia Pradic September 2025 The Cantor-Bernstein theorem states that sizes of sets can be compared meaningfully using injections: if Ainjects into Band vice-versa, Aand Bare in bijection. This is typically proven via an explicit construction that does not involve choice, but the proof cannot be constructive. For instance, [0,1] and (0,1) can be embedded into one another but are not homeomorphic, meaning that Cantor-Bernstein is violated in a number of models of intuitionistic set theory. Faced with this state of affairs, we can still ask: how bad is it? First, we are going to see how Cantor-Bernstein implies full excluded middle. We will then turn our attention to the Myhill isomorphism theorem, a constructive version of CantorBernstein that states that, for any two subsets A, B ⊆Nthat are inter-reducible via injections, there is a bijection N→Nthat preserves them. The theorem remains true classically if Nis replaced by an arbitrary set X, but this is not the case constructively. Bauer asked if there is a nice class of sets Xfor which it does hold constructively. After checking there is no hope for this class of sets to be closed under basic operations like disjoint unions, we will see that a version of this generalized Myhill isomorphism theorem holds for the conatural numbers N∞by adapting the usual back-and-forth construction and assuming Markov’s principle. However, this does not extend much: this fails for 2 ×N∞,N+N∞as well as Cantor space. We are going to see why those failures are of different flavours, and sketch how this could be made more precise by using oracle modalities. Based on joint work with Chad Brown: arXiv:1904.09193 and arXiv:2507.05028. 1