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.

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.

Equations

$$\epsilon :({\mathbb{N}}_{\infty }\to 2)⟶{\mathbb{N}}_{\infty }$$

$$\big{(}\forall p\in{\mathbb{N}_{\infty}}.\;P(p)=1\big{)}\qquad\Longleftrightarrow\qquad P(\varepsilon(P))=1$$

$$g(y):=\left\{\begin{array}[]{ll}x&{\mbox{ if }}f(x)=y\\ d&{\mbox{ if no such }}x{\mbox{ exists}}\end{array}\right.$$

$$\forall i\in 2.g(i)=\mathsf{inl}(0)\vee g(i)=\mathsf{inr}(0)$$

$$\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\\\crcr}}}\ignorespaces{\hbox{\kern-5.5pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{1\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern-2.72223pt\raise-9.81943pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{+}$}}}}}\ignorespaces{}{\hbox{\kern-6.75pt\raise-19.63887pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A}$}}}}}}}\ignorespaces}}}}\ignorespaces}\left\{\quad\vbox{ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-5.5pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern-6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}\ignorespaces}}}}\ignorespaces}\quad\right\}2\hskip 20.0pt\longmapsto\hskip 20.0pt\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-5.5pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 5.50002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces}\text{\quad or \quad}\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-5.5pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 6.8889pt\raise-13.41061pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 5.50002pt\raise-2.49219pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces}\text{\quad or \quad}\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\}}}\ignorespaces{\hbox{\kern-5.5pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet}$}}}}}}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 5.50002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern-6.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\divideontimes}$}}}}}}}{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 5.50002pt\raise-2.49219pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces}}}}\ignorespaces}$$

$$\divideontimes \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr\\\crcr}}}\ignorespaces{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern-2.72223pt\raise-21.41666pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{+}$}}}}}\ignorespaces{}{\hbox{\kern-6.75pt\raise-42.83331pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\mathbb{N}}$}}}}}}}\ignorespaces}}}}\ignorespaces}\left\{\quad\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 6.8889pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&\\&\\&\\&\\&\\}}}\ignorespaces{\hbox{\kern-6.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\divideontimes\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern 30.8889pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 5.50002pt\raise-14.0413pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-5.5pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.8889pt\raise-16.53886pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 5.50002pt\raise-29.64687pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-5.5pt\raise-31.98329pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\bullet\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 30.8889pt\raise-31.98329pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 30.8889pt\raise-31.98329pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\bullet}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\kern 3.0pt\raise-44.11566pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawline@}}\ignorespaces{\hbox{\lx@xy@drawline@}}{\hbox{\kern-3.0pt\raise-45.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern 15.56944pt\raise-45.2055pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\vdots}$}}}}}\ignorespaces{}{\hbox{\kern 33.3889pt\raise-45.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-3.0pt\raise-56.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern 15.56944pt\raise-56.2055pt\hbox{\hbox{\kern 0.0pt\raise-1.75pt\hbox{$\scriptstyle{\vdots}$}}}}}\ignorespaces{}{\hbox{\kern 33.3889pt\raise-56.2055pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces}\quad\right\}\mathbb{N}\hskip 40.0pt\begin{array}[]{lrclcllcl}f:&\mathbb{N}&\longrightarrow&A+\mathbb{N}\\ &n&\mapsto&{\sf inr}(n)\\ &&&\\ g:&A+\mathbb{N}&\longrightarrow&\mathbb{N}\\ &{\sf inl}(0)&\mapsto&0\\ &{\sf inr}(n)&\mapsto&n+1\par\end{array}$$

$$\forall p\in 2^O.(\exists x\in O.p(x)=0)\vee (\forall x\in O.p(x)=1)$$

$$p(x)=\left\{\begin{array}[]{lr}0&{\mbox{ if }}\exists a\in A.\;f(x)={\sf inl}(a)\\ 1&{\mbox{ if }}\exists b\in B.\;f(x)={\sf inr}(b)\end{array}\right.$$

$${\mathbb{N}_{\infty}}=\big{\{}p\in 2^{\mathbb{N}}\mathrel{\big{|}}\forall n\in\mathbb{N}.\leavevmode\nobreak\ \big{(}p(n)=1\;\Rightarrow\;\forall m\in\mathbb{N}.\leavevmode\nobreak\ (m<n\;\Rightarrow\;p(m)=1)\big{)}\big{\}}.$$

$$\underline{n}(m)=\left\{\begin{array}[]{lr}1&{\mbox{ if }}m<n\\ 0&{\mbox{ otherwise.}}\end{array}\right.$$

$$\varepsilon(Q)(n)=\left\{\begin{array}[]{lr}1&{\mbox{ if }}Q(\underline{k}){\mbox{ for each }}k\leq n\\ 0&{\mbox{ otherwise.}}\end{array}\right.$$

$$\begin{array}[]{lcclcccl}f:&{\mathbb{N}_{\infty}}&\longrightarrow&A+{\mathbb{N}_{\infty}}&\phantom{aaaaaaa}g:&A+{\mathbb{N}_{\infty}}&\longrightarrow&{\mathbb{N}_{\infty}}\\ &x&\mapsto&{\sf inr}(x)&&{\sf inl}(0)&\mapsto&\underline{0}\\ &&&&&{\sf inr}(x)&\mapsto&\underline{{\sf S}}(x)\end{array}$$

Full text

The Cantor-Bernstein theorem is an elementary statement ${\mathbb{CB}}$ of set theory: for any two sets $A$ and $B$, if there are injections $f:A\hookrightarrow B$ and $g:B\hookrightarrow A$, then there exists a bijection $h:A\xrightarrow{\sim}B$. An interesting feature of this theorem is that it may be proven in ZF without assuming the axiom of choice. However, this proof is non-constructive in the sense that it goes through classical logic; while the construction of the bijection $h$ is rather explicit, one needs to appeal to excluded middle to show that it is indeed a bijective function.

Models of constructive set theory invalidating ${\mathbb{CB}}$ are known, such as for instance, models based on Kleene realizability111For instance, consider the subset $H\subseteq\mathbb{N}$ corresponding to the halting problem. If ${\mathbb{CB}}$ held in the effective topos, we would have a recursive bijection $\mathbb{N}\xrightarrow{\sim}\{2n\mathrel{|}n\notin H\}\cup\{2n+1\mathrel{|}n\in\mathbb{N}\}$; since it is in particular surjective, we would be able to build a recursive enumeration of the complement of $H$, which is absurd.. However, this still left open the question of whether the full power of excluded middle $({\mathbb{EM}})$ is really necessary to prove the theorem or if a weaker classical principle would be enough. The purpose of this note is to show that, indeed, full excluded middle is required.

The argument is a straightforward application of a key theorem of Martín Escardó [Esc13] concerning the one-point compactification ${\mathbb{N}_{\infty}}$ of $\mathbb{N}$ and decidable predicates: there exists a function

[TABLE]

selecting a counter-witness for its input when possible. Formally speaking, it means that for any decidable predicate $P:{\mathbb{N}_{\infty}}\to 2$, we have the following equivalence222This should not be confused with Hilbert’s $\varepsilon$ which dually selects witnesses of existential statements..

[TABLE]

This result is rather striking as it means that there exists an infinite set333By which we systematically mean Dedekind-infinite here. for which decidable predicates are stable under quantification, provably in constructive logic. This is to be contrasted against the case of $\mathbb{N}$, which admits no recursive selection function.

Assuming the existence of any infinite set equipped with a selection function, ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$ may be proven by very elementary means. The reader familiar with [Esc13] may content themselves with the proofs of Lemma 3.2 and Theorem 1. Section 3 as a whole gives a self-contained proof of ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$, integrating the necessary technical content from [Esc13] about ${\mathbb{N}_{\infty}}$. For the more casual reader, we first give a preliminary example of an elementary set-theoretic statement implying excluded middle in Section 1, so as to illustrate how many similar statements can be proven because of the comprehension axiom. We then give an already-known proof [Ban86] of a weaker variant of Theorem 1 in Section 2 for didactic purposes, before moving on to the proof of Theorem 1.

Foundational and notational preliminaries

We work informally in an intuitionistic set theory such as IZF where we do not assume excluded middle upfront; we essentially require that the usual axioms of Zermelo’s set theory hold [Myh73], including full separation. Among other things, this means that our universe of sets is closed under pairing, union, powerset (which we write $\mathcal{P}(-)$) and set comprehension $\{x\in A\mid\varphi\}$. For sets $A$ and $B$, function spaces $B^{A}$ and disjoint unions $A+B$ are built as usual. We write ${\sf inl}:A\to A+B$ and ${\sf inr}:B\to A+B$ for the usual injections into disjoint unions. In particular, for every $x\in A+B$ there is either an $a\in A$ such that $x={\sf inl}(a)$ or $b\in B$ such that $x={\sf inr}(b)$. We let [math] be the empty set $\emptyset$, $1=\{0\}$ and $2=\{0,1\}\cong 1+1$.

In set theory, propositions or truth values can be arranged as a set $\Omega=\mathcal{P}(1)$, which is closed under all logical connective. For a formal proposition $p\in\Omega$, we sometimes abbreviate “$p=1$” by “$p$” when writing formulas. Excluded middle ${\mathbb{EM}}$ may then be formally written as $\forall p\in\Omega.\;p\vee\neg p$444Note that the scheme $\forall x.\;\varphi(x)\vee\neg\varphi(x)$ for arbitrary $\varphi$ can be recovered by set comprehension.. Note that an equivalent formulation of ${\mathbb{EM}}$ in this setting is $\Omega\cong 2$, which is not the case in constructive settings. In the sequel, although they are definitionally the same in set theory, we often make a notational distinction between propositions $p\in\Omega$ and subsets $A\subseteq 1$ for readability.

Finally, and crucially555Interestingly, one may easily construct models of finitary models satisfying ${\mathbb{CB}}$ but not ${\mathbb{EM}}$: take the internal logic of the topos ${\sf Finset}^{\mathcal{C}^{\text{op}}}$. If $\mathcal{C}$ is not a groupoid, ${\mathbb{EM}}$ is not satisfied, while ${\mathbb{CB}}$ always hold in the internal logic. This indicates that assuming the axiom of infinity is essential here., we assume the axiom of infinity and call $\mathbb{N}$ the set of natural numbers.

Related works

We do not reprove ${\mathbb{EM}}\Rightarrow{\mathbb{CB}}$ here; while it is not necessary to read this note, they motivate a strengthening of ${\mathbb{CB}}$ mentioned in Definition 2.1. Any introduction to set theory should have a satisfactory proof; for reference, one may look at [Jec13, Theorem 3.2]. For a historical perspective, the reader may be interested in Hinkis’ monograph [Hin13]. The question of the non-constructiveness of ${\mathbb{CB}}$ from the categorical point of view was studied by Banaschewski and Brümmer in [Ban86] and mentioned in Johnstone’s Elephant [Joh02, Lemma D4.1.12, p.950].

Since the first version of this note, Martín Escardó carried out further investigations regarding Cantor-Bernstein and excluded middle in the context of type theory; the Agda formalization [Esc20] includes a wealth of further results in addition to a generalization of ${\mathbb{CB}}$ to $\infty$-groupoids[Esc21].

Acknowledgements

Thanks to Robert Passman who signaled us a misleading statment in the initial version of this document, which misguidedly mentioned CZF (full separation is needed here if we want full ${\mathbb{EM}}$) and to Jim Kingdon for reporting mistaken type annotations. Let us also thank (belatedly) Andrej Bauer and Henryk Michalewski for pushing us to put this out there and Martín Escardó for follow-up discussions. Also many thanks to them and the broader community for their inspiring work!

1 An elementary set-theoretic statement implying ${\mathbb{EM}}$

Let us start with an example of a statement involving functions, which could very well be given as a exercise in a first introduction to set theory.

Proposition 1.1**.**

Let $A$ and $B$ be sets and $f:A\to B$ an injective function. Suppose that $A$ is non-empty. If excluded middle holds, then there exists a surjection $g:B\to A$.

Proof.

Since $A$ is non-empty, one can pick a default element $d\in A$. By excluded middle, we know for every $y\in B$ either there exists an $x\in A$ such that $f(x)=y$ or no such $x$ exists. Hence we can define $g$ by cases as follows:

[TABLE]

Note $g$ is well defined since $f$ is injective, and $g$ is clearly surjective. ∎

Notice that in this little proof, one needs to make a case analysis using excluded middle. As in the case of Cantor-Bernstein, one can ask if this is necessary. It is in our setting.

Proposition 1.2**.**

Suppose for all sets $A$ and $B$ there is a surjective function $g:B\to A$ whenever $A$ is nonempty and there is an injective function $f:A\to B$. Then excluded middle holds.

Proof.

Let $p\in\Omega$ be given and consider $A\mathrel{:=}\{0\mathrel{|}p\}$. There is clearly an injection $f:A+1\to 2$ given by $f({\sf inl}(x))=0$ for $x\in A$ and $f({\sf inr}(0))=1$. Note that $A+1$ is non-empty, as ${\sf inr}(0)\in A+1$. Applying our assumption, we obtain a surjection $g:2\to A+1$. Note that

[TABLE]

holds because of the universal property of disjoint unions. Hence we have two cases.

• •

Suppose $g(i)={\sf inl}(0)$ for some $i\in 2$. In this case $0\in A$ and so $p$ holds.

• •

Suppose $g(0)={\sf inr}(0)$ and $g(1)={\sf inr}(0)$. We prove $\neg p$ holds. To this end, assume $p$ holds. Hence $0\in A$. Since $g$ is surjective there must be some $i\in 2$ such that $g(i)={\sf inl}(0)$, contradicting our assumption.

∎

Here, the strategy was fairly simple: take the $A\subseteq 1$ associated to the proposition, and try to make it fit in the hypothesis of the lemma using disjoint unions and singletons. The situation in the proof can be visualized as follows:

[TABLE]

2 Reversing Cantor-Bernstein-Banaschewski-Brümmer

One can try to adopt a similar strategy for proving that Cantor-Bernstein implies excluded middle.

Provided some $A\subseteq 1$, one can start building an injection $f:A\to 1$.

[TABLE]

However, we need to have an injection going back and we are unsure of the existence of an element in $A$. So let us consider the obvious injection $1\to A+1$.

[TABLE]

Again we need a new value to be the image under $f$ of this latest element, which leads us to consider $2$. Since we still do not have two injections, one might be tempted to iterate this process.

[TABLE]

This informal discussion suggests using $\mathbb{N}$ and the following injections.

[TABLE]

${\mathbb{CB}}$ then provides a bijection $h:\mathbb{N}\to A+\mathbb{N}$. In fact, in elementary proofs of the theorem this bijection can be seen as a perfect matching of the above graph. Note however that the usual statement ${\mathbb{CB}}$ conceals this relationship between $f,g$ and $h$. Banaschewski and Brümmer [Ban86] studied the corresponding strengthened version of ${\mathbb{CB}}$, which we dub ${\mathbb{CBBB}}$, in a categorical setting and proved that it implied excluded middle.

Definition 2.1**.**

We say ${{\mathbb{CBBB}}}$ holds if the following statement holds: given sets $A$ and $B$ and injections $f:A\to B$ and $g:B\to A$, there is a bijection $h:A\to B$ such that for all $x\in A$ and $y\in B$, $f(x)=y$ or $x=g(y)$ whenever $h(x)=y$.

Let us remark that it is obvious that ${\mathbb{CBBB}}\Rightarrow{\mathbb{CB}}$. Let us also stress that ${\mathbb{EM}}\Rightarrow{\mathbb{CBBB}}$ can be easily obtained by adapting elementary proofs of ${\mathbb{EM}}\Rightarrow{\mathbb{CB}}$.

Theorem 2.2** (Proposition 4.1 in [Ban86]).**

If ${{\mathbb{CBBB}}}$ holds, then excluded middle holds.

Proof.

Assume ${{\mathbb{CBBB}}}$ holds. Let a proposition $p\in\Omega$ be given, seen as a subset $A=\{0\mathrel{|}p\}\subseteq 1$. Take $f:\mathbb{N}\to A+\mathbb{N}$ and $g:A+\mathbb{N}\to\mathbb{N}$ to be the injections described above.

By ${{\mathbb{CBBB}}}$ there is a bijection $h:\mathbb{N}\to A+\mathbb{N}$ such that $f(x)=y$ or $g(y)=x$ whenever $h(x)=y$ for $x\in\mathbb{N}$ and $y\in A+\mathbb{N}$. We know either $h(0)={\sf inl}(0)$ or $h(0)={\sf inr}(n)$ for some $n\in\mathbb{N}$.

• •

If $h(0)={\sf inl}(0)$, then $0\in A$ and so $p$ holds.

• •

Suppose $h(0)={\sf inr}(n)$ for some $n\in\mathbb{N}$. We will prove $\neg p$ holds. To this end, assume $p$ holds, so that $0\in A$. Since $h$ is surjective, there is some $m\in\mathbb{N}$ such that $h(m)={\sf inl}(0)$. Either $f(m)={\sf inl}(0)$ or $g({\sf inl}(0))=m$. The first case is impossible since $f(m)={\sf inr}(m)$ by the definition of $f$ and ${\sf inl}(0)\not={\sf inr}(m)$. Therefore, $g({\sf inl}(0))=m$ and, by definition of $g$, we must have $m=0$. This is also impossible since it implies ${\sf inl}(0)=h(m)=h(0)={\sf inr}(n)$.

∎

3 Reversing Cantor-Bernstein

Let us pause a moment and consider why we failed to prove the analogue of Proposition 1.2. In that proof of that proposition lemma, we did not use any information about the surjection $g$. Instead, we resorted to exhaustively enumerating the set $2$ to check whether we had some $x\in 2$ such that $g(x)={\sf inr}(0)$, which is a decidable property. This feature of $2$ of being searchable may be formalized using the notion of omniscience.

Definition 3.1** (Omniscient sets).**

We say a set $O$ is omniscient if for every $p\in 2^{O}$ if either there exists $x\in O$ such that $p(x)=0$, or $p$ is constantly equal to $1$. That is,

[TABLE]

In classical logic, all sets are clearly omniscient, but this is not necessarily true in constructive logics. However, all finite sets, and in particular $2$, are omniscient. This concept allows us to isolate the actual core of the proof of Proposition 1.2.

Lemma 3.2**.**

Suppose that we have an omniscient set $O$ and some sets $A$ and $B$. If there exists a surjection $f:O\to A+B$, then either $A$ is inhabited or it is empty.

Proof.

Let $f:O\to A+B$ be given and define $p\in 2^{O}$ by

[TABLE]

Since $O$ is omniscient either $\exists x.\;P(x)=0$ or $\forall x\in O.\;P(x)=1$. If $\exists x\in O.\;P(x)=0$, then $A$ is clearly inhabited. Suppose $P(x)=1$ for every $x\in O$. We show that $A$ is empty. Suppose that we have $a\in A$ toward a contradiction. Since $f$ is surjective, there is some $x\in O$ such that $f(x)={\sf inl}(a)$ and thus $P(x)=0$. This contradicts $P(x)=1$. ∎

From ${{\mathbb{CB}}}$ (instead of the stronger ${{\mathbb{CBBB}}}$) we could use the injections from the proof of Theorem 2.2 to obtain a surjection $\mathbb{N}\to A+\mathbb{N}$. If $\mathbb{N}$ were omniscient, then we could use this surjection with Lemma 3.2 to ${\mathbb{EM}}$. However, omniscience of $\mathbb{N}$ correspond to the axiom of limited principle of omniscience (${\mathbb{LPO}}$) a well-known constructive taboo [Bis67], which can be thought of as a (strictly weaker) version of ${\mathbb{EM}}$666 Remark that, at this point, we have ${\mathbb{LPO}}\wedge{\mathbb{CB}}\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ {\mathbb{EM}}$ over constructive set theory. This observation is however not necessary to carry out the subsequent argument.. This means that deriving ${\mathbb{EM}}$ from the existence of bijections $\mathbb{N}\cong 1+\mathbb{N}$ by way of Lemma 3.2 is unreasonable. Luckily for us, Escardó proved that there exists an infinite subset of the Cantor space, ${\mathbb{N}_{\infty}}$, which is omniscient [Esc13] and can be used to prove ${\mathbb{CB}}\Rightarrow{\mathbb{EM}}$.

In order to keep the argument self-contained, we reproduce his argument below before deriving the main result.

Definition 3.3**.**

We define ${\mathbb{N}_{\infty}}$ to be the set of non-increasing sequences in $2^{\mathbb{N}}$, i.e.777For more categorically-inclined people, ${\mathbb{N}_{\infty}}$ is the final coalgebra for the functor $X\mapsto 1+X$. This would justify calling ${\mathbb{N}_{\infty}}$ the set of conatural numbers. On the other hand, the induced topology from $2^{\mathbb{N}}$ in Definition 3.3 also justifies calling ${\mathbb{N}_{\infty}}$ the one-point compactification of $\mathbb{N}$ (seen as a discrete space).,

[TABLE]

Let $\omega\in{\mathbb{N}_{\infty}}$ denote the constant function $n\mapsto 1$. Define an injection taking $n\in\mathbb{N}$ to $\underline{n}\in{\mathbb{N}_{\infty}}$ by

[TABLE]

Finally, define $\underline{{\sf S}}:{\mathbb{N}_{\infty}}\to{\mathbb{N}_{\infty}}$ by setting $\underline{{\sf S}}(p)(0)=1$ and $\underline{{\sf S}}(p)(n+1)=p(n)$.

The set ${\mathbb{N}_{\infty}}$ is infinite as witnessed by $\underline{0}$ and $\underline{{\sf S}}$.

Lemma 3.4**.**

The function $\underline{{\sf S}}:{\mathbb{N}_{\infty}}\to{\mathbb{N}_{\infty}}$ is injective and $\underline{{\sf S}}(p)\not=\underline{0}$ for all $p\in{\mathbb{N}_{\infty}}$.

Proof.

Suppose $\underline{{\sf S}}(p)=\underline{{\sf S}}(q)$. Since $p(n)=\underline{{\sf S}}(p)(n+1)=\underline{{\sf S}}(q)(n+1)=q(n)$ for every $n\in\mathbb{N}$ we know $p=q$, as desired. The fact that $\underline{{\sf S}}(p)\not=\underline{0}$ for all $x\in{\mathbb{N}_{\infty}}$ follows from $\underline{{\sf S}}(p)(0)=1\not=0=\underline{0}(0)$. ∎

Classically every element of ${\mathbb{N}_{\infty}}$ is either $\omega$ or of the form $\underline{n}$. The corresponding disjunction is equivalent to ${\mathbb{LPO}}$, and so is unprovable constructively. However, for decidable predicates, it is sufficient to show that they hold over all elements $\underline{n}$ and $\omega$ to show they hold everywhere888This constitutes a particular case of Lemma 3.4 in [Esc13]..

Lemma 3.5**.**

Let $Q\in 2^{\mathbb{N}_{\infty}}$ be given. If $Q(\omega)=1$ and $\forall n\in\mathbb{N}.\leavevmode\nobreak\ Q(\underline{n})=1$, then $\forall p\in{\mathbb{N}_{\infty}}.\leavevmode\nobreak\ Q(p)=1$.

Proof.

Let $Q\in 2^{\mathbb{N}_{\infty}}$ such that $Q(\omega)=1$ and $\forall n\in\mathbb{N}.\leavevmode\nobreak\ Q(\underline{n})=1$. Let $p\in{\mathbb{N}_{\infty}}$ be given. To prove $Q(p)=1$, it is enough to prove $Q(p)\not=0$. Assume $Q(p)=0$. Under this assumption we can prove $\forall n\in\mathbb{N}.\leavevmode\nobreak\ p(n)=1$ by strong induction. Assume $\forall k\in\mathbb{N}.\leavevmode\nobreak\ (k<n\Rightarrow p(k)=1)$ and $p(n)=0$. This is enough information to infer $p=\underline{n}$, contradicting $Q(p)=0$ and $Q(\underline{n})=1$. To end the proof we note that $p$ must be $\omega$ (since $\forall n\in\mathbb{N}.\leavevmode\nobreak\ p(n)=1$), contradicting $Q(p)=0$ and $Q(\omega)=1$. ∎

While the desired selection function $\varepsilon:2^{{\mathbb{N}_{\infty}}}\to{\mathbb{N}_{\infty}}$ is rather easy to define effectively, Lemma 3.5 is critical in allowing to prove constructively that it is indeed a selection function.

Theorem 3.6** ([Esc13, Theorem 3.15]).**

There is a function $\varepsilon:2^{{\mathbb{N}_{\infty}}}\to{\mathbb{N}_{\infty}}$ such that for every $Q\in 2^{{\mathbb{N}_{\infty}}}$, if $Q(\varepsilon(Q))=1$, then $\forall p\in{\mathbb{N}_{\infty}}.\leavevmode\nobreak\ Q(p)=1$.

Proof.

For $Q\in 2^{{\mathbb{N}_{\infty}}}$, take $\varepsilon(Q)\in 2^{\mathbb{N}}$ to be

[TABLE]

This is well-defined by recursion over $n$. It is easy to check that $\varepsilon(Q)\in{\mathbb{N}_{\infty}}$ as well.

Assume $Q(\varepsilon(Q))=1$ and let $p\in{\mathbb{N}_{\infty}}$ be given. If $\forall k<n.\;Q(\underline{k})=1$ and $Q(\underline{n})=0$, then $\varepsilon(Q)=\underline{n}$ and so $Q(\underline{n})=Q(\varepsilon(Q))=1$, contradicting $Q(\underline{n})=0$. Consequently, an induction proves that $Q(\underline{n})=1$ for every $n\in\mathbb{N}$. Thus $\varepsilon(Q)=\omega$ and so $Q(\omega)=Q(\varepsilon(Q))=1$ holds as well. Hence $Q(p)=1$ for every $p\in{\mathbb{N}_{\infty}}$ by Lemma 3.5. ∎

Corollary 3.7** ([Esc13, Corollary 3.6]).**

The set ${\mathbb{N}_{\infty}}$ is omniscient.

Proof.

Let $Q\in 2^{{\mathbb{N}_{\infty}}}$ be given. If $Q(\varepsilon(Q))=0$, then $\exists x\in{\mathbb{N}_{\infty}}.Q(x)=0$. If $Q(\varepsilon(Q))=1$, then $\forall x\in{\mathbb{N}_{\infty}}.\;Q(x)=1$ by Theorem 3.6. ∎

This completes the part of the construction we obtained following Escardó [Esc13]. We can now easily put it together with Lemma 3.2 to conclude.

Proof of Theorem 1.

Assume ${{\mathbb{CB}}}$ holds. We know ${\mathbb{N}_{\infty}}$ is omniscient by Lemma 3.7. We know $\underline{{\sf S}}$ is injective and $\underline{{\sf S}}(x)\not=\underline{0}$ for every $x\in{\mathbb{N}_{\infty}}$ by Lemma 3.4. Let $p\in\Omega$ be a proposition and take $A=\{0\mathrel{|}p\}\subseteq 1$. Analogously to Section 2, we consider the following functions:

[TABLE]

Both $f$ and $g$ are clearly injective, so we can apply ${{\mathbb{CB}}}$ to obtain a bijection $h:{\mathbb{N}_{\infty}}\to A+{\mathbb{N}_{\infty}}$. Lemma 3.2 now implies that either $A$ is inhabited (so $p$ holds) or $A$ is empty (so $\neg p$ holds). ∎