English

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 2N2^{\mathbb{N}}, the so-called one-point compactification of N\mathbb{N}, preserves decidable predicates.

Keywords

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

R2 v1 2026-06-23T08:44:45.511Z