How unconstructive is the Cantor-Bernstein theorem?

Abstract: Based on joint work with Chad Brown [1] and [2]. The Cantor-Bernstein theorem states that sizes of sets can be compared meaningfully using injections: if A injects into B and vice-versa, A and B are 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 it is? 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 Cantor-Bernstein that states that, for any two subsets A, B ⊆ ℕ that are inter-reducible via injections, there is a bijection ℕ → ℕ that preserves them. The theorem remains true classically if ℕ is replaced by an arbitrary set X, but this is not the case constructively. Bauer asked if there is a nice class of sets X for 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 ℕ∞ by adapting the usual back-and-forth construction and assuming Markov's principle. However, this does not extend much: this fails for 2× ℕ∞, ℕ + ℕ∞ as well as Cantor space. We are going to see why those failures are of different flavours, and sketch how to make this more precise by using oracle modalities.

1. Pradic, C. and Brown, C. E. 2022. Cantor-Bernstein implies Excluded Middle. arXiv preprint arXiv:1904.09193.

2. Pradic, C. 2025. The Myhill isomorphism theorem does not generalize much. arXiv preprint arXiv:2507.05028.

logic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic