Cantor-Bernstein implies Excluded Middle

arXiv1904.09193MaRDI QIDQ6317469FDOQ6317469

Authors: Cécilia Pradic, Chad E. Brown 

Publication date: 19 April 2019

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^{mathbbN}$, the so-called one-point compactification of $mathbbN$, preserves decidable predicates.

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

This page was built for publication: Cantor-Bernstein implies Excluded Middle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6317469)