We prove in constructive logic that the statement of the Cantor-Bernstein theorem implies excluded middle. This establishes that the Cantor-Bernstein theorem can only be proven assuming the full power of classical logic. The key ingredient is a theorem of Mart\'in Escard\'o stating that quantification over a particular subset of the Cantor space $2^{ \mathbb{ N}}$, the so-called one-point compactification of $\mathbb{ N}$, preserves decidable predicates.
Categories: math.LO cs.LO