Cantor-Bernstein implies Excluded Middle

04/19/2019
by   Pierre Pradic, et al.
0

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ín Escardó stating that quantification over a particular subset of the Cantor space 2^N, the so-called one-point compactification of N, preserves decidable predicates.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset