arXiv · 1904.09193
Cantor-Bernstein implies Excluded Middle
Abstract
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.
Explore related subjects
Keep this discovery
Cécilia Pradic, Chad E. Brown. 2019-04-19. Cantor-Bernstein implies Excluded Middle. https://arxiv.org/abs/1904.09193
Cite the original work for its findings. Save a collection to share your selection of sources.