# Cantor-Bernstein implies Excluded Middle

## TL;DR

This paper demonstrates that in constructive logic, the Cantor-Bernstein theorem implies the law of excluded middle, showing it cannot be proven without classical logic assumptions.

## Contribution

It establishes a logical equivalence between the Cantor-Bernstein theorem and excluded middle within constructive logic, highlighting the theorem's reliance on classical principles.

## Key findings

- Cantor-Bernstein implies excluded middle in constructive logic
- The proof uses a theorem on quantification over the one-point compactification of natural numbers
- The result clarifies the logical strength of the Cantor-Bernstein theorem

## 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.