Cantor-Bernstein implies Excluded Middle
Logic
2023-03-24 v3 Logic in Computer Science
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 , the so-called one-point compactification of , preserves decidable predicates.
Cite
@article{arxiv.1904.09193,
title = {Cantor-Bernstein implies Excluded Middle},
author = {Cécilia Pradic and Chad E. Brown},
journal= {arXiv preprint arXiv:1904.09193},
year = {2023}
}
Comments
6pp / update: corrected an error in the intro wrt applicability of Thm 1, typos, added a couple of acks and a ref