Is there a constructive proof of Cantor–Bernstein–Schroeder theorem ?

Question

An important feature of the Cantor-Schroeder-Bernstein theorem is that it does not rely on the axiom of choice. However, its various proofs are non-constructive, as they depend on the law of excluded middle.

There are several well-known proof strategies. For example, there is a simple proof which uses Tarski's fixed point theorem.

My question pertains to the well known proof attributed to Julius Konig, and given here: Proof by Konig. What I have not been able to grasp is, how this is not a constructive proof? Given functions $f$ and $g$, isn't it possible to actually arrive at the bijection by forming biinfinite sequences as given in the proof?

Answer 1

There is no constructive proof.

To show this, let $A = \mathbb{N}$ and let $B = \{ n \in \mathbb{N}\; |\; \varphi_n(0) \uparrow \}$, where $\varphi_n(0) \uparrow$ means that the $n$th Turing machine is undefined on input 0. There are computable injections $f:A \rightarrow B$ and $g:B \rightarrow A$ (the identity), but no computable surjection from $A$ to $B$ because $B$ is not a c.e. set.

To see why Konig's proof is nonconstructive, let's say that we want to know what the image of $n \in A$ is under the bijection. In order to do this we need to know whether we apply $f$ or $g^{-1}$. But to know this we need to decide whether $n$ is an $A$-stopper, a $B$-stopper, or neither. However we can't do this constructively because it would require checking the entire possibly infinite sequence to see if it ever stops. In fact, in the example above, being able to decide whether or not $g^{-1}$ is defined is the same as deciding the halting problem, so at odd stages we don't even know whether or not the sequence extends any further back at all.

Answer 2

The Cantor-Bernstein-Schröder theorem (did I read somewhere that Dedekind was the first to prove it?) is not valid constructively. Here are a couple of reasons why.

There are models in which the theorem fails

Here is a pretty one. In the realizability topos over the infinite-time Turing machines there is an injection $\mathbb{R} \to \mathbb{N}$. Because the topos satisfies countable choice there is no surjection $\mathbb{N} \to \mathbb{R}$ (hence no bijection), but there clearly is an injection $\mathbb{N} \to \mathbb{R}$.

Todd mentioned a presheaf model in his answer.

The usual proofs are non-constructive

You asked what is non-constructive about König's proof. It uses excluded middle several times:

1. "the sequence can be extended on the left, depending on whether $a$ is in the image of $g$ or not",
2. "the sequence constructed in the proofs either terminates or not",
3. "the sequences so constructed partition the disjoint union of the two sets".

For a proof which uses excluded middle in a more controled way, see the one using Tarski's fixed point theorem, as outlined here. Excluded middle is used "only" in the last step, when the bijection $i$ is defined, depending on whether an element is in $C$ or not.

The theorem implies strange things, constructively speaking

Here is a strange consequence of the theorem, I will try to improve on it but do not have the time right now. Consider the Cantor space $C = 2^\mathbb{N}$ and the subspace of those sequences which contain a 1, $D = \lbrace \alpha \in C \mid \exists n . \alpha n = 1\rbrace$. As there are injections $C \to D$ and $D \to C$ there is a bijection $h : C \to D$. That is very strange, for it is consistent to assume that all maps on $C$ are uniformly continuous, but such a bijection cannot be uniformly continuous. I will try to improve on this.

Answer 3

If you accept that toposes are models of constructive set theory, then another way to answer the question is to give a (non-Boolean) topos where the CBS theorem fails; that would show that this theorem can't possibly have a constructive proof.

A simple example of such a topos is the arrow category $Set^\to$, whose objects are functions $X_0 \to X_1$ between sets and whose morphisms are commutative squares. Let $X$ be the object $f: \mathbb{N} \to \mathbb{N}$ that takes $n \in \mathbb{N}$ to $\mathrm{int}(n/2)$, where $\mathrm{int}(x)$ is the greatest integer less than or equal to $x$; let $Y$ be the object $g: \mathbb{N} \to \mathbb{N}$ that takes $n$ to $\mathrm{Int}((n+1)/2)$, where $\mathrm{Int}(x)$ is the least integer greater than or equal to $x$. It is pretty clear that $X$ and $Y$ are non-isomorphic, because $g^{-1}(0)$ has cardinality $1$ where all fibers of $f$ have cardinality $2$. But, just by drawing pictures of these objects, it is easy to construct monomophisms $i: X \to Y$ and $j: Y \to X$ (e.g., define $i_0(n) = n+1$ and $i_1(n) = n+1$ for all $n$, and define $j_0(n) = n+1$ for $n \gt 0$, $j_0(0) = 0$, and $j_1(n) = n$ for all $n$).

---

For people who are not used to thinking of topos theory as "constructive set theory", there is another way of considering the example above in terms of "$H$-valued sets", where $H$ is the Heyting algebra with three elements, $H = \{0 < 1/2 < 1\}$. The law of the excluded middle does not hold; one can easily calculate $\neg \neg (1/2) = 1$.

An $H$-valued set is a set $X$ together with a function $e_X: X \times X \to H$ which measures the extent to which elements of $X$ are considered "equal", subject to transitivity and symmetry axioms:

$$e_X(x, y) \wedge e_X(y, z) \leq e_X(x, z), \qquad e_X(x, y) = e_X(y, x).$$

We can think of $e_X(x, x)$ as measuring the extent to which $x$ "exists". An $H$-valued relation is a function $r: X \times Y \to H$ such that

$$e_X(x', x) \wedge r(x, y) \leq r(x', y), \qquad r(x, y) \wedge e_Y(y, y') \leq r(x, y'), \qquad r(x, y) \leq e_X(x, x) \wedge e_Y(y, y).$$

An $H$-valued function $f: X \to Y$ is an $H$-valued relation such that

$$f(x, y) \wedge f(x, y') \leq e_Y(y, y'), \qquad e_X(x, x) \leq \bigvee_{y \in Y} f(x, y)$$

where the first condition is an analogue of well-definedness and the second roughly says that $f(x)$ is defined to the extent $x$ exists. It turns out that the category of $H$-valued sets is equivalent to the topos $Set^\to$.

Under this equivalence, $X$ in the example above is identified with the pair $(\mathbb{N}, e_X: \mathbb{N} \times \mathbb{N} \to H)$ where $e_X(n, n) = 1$, where $e_X(m, n) = 1/2$ if $m \neq n$ but $f(m) = f(n)$, and otherwise $e_X(m, n) = 0$. There is a similar description of $Y$ in terms of $H$-valued sets. For such $H$-valued sets where $e_X(x, x') = 1$ for all precisely when $x = x'$, functional $H$-relations between them can be described as actual functions $f: X \to Y$ subject to the condition $e_X(x, x') \leq e_Y(f(x), f(x'))$ for all $x, x'$ in $X$.

The monomorphic functional relations $i: (\mathbb{N}, e_X) \to (\mathbb{N}, e_Y)$ and $j: (\mathbb{N}, e_Y) \to (\mathbb{N}, e_X)$ turn out to be given by $i(n) = n+1$ and $j(0) = 0$, $j(n) = n+1$ for $n > 0$ (i.e., the functions $i_0$ and $j_0$ in the example above). The monomorphicity amounts to the condition that $e_Y(i(x), i(x')) = e_X(x, x')$ for all $x, x'$ in $X$ (and similarly for $j$). This is easily checked.

Now one can try to run through the König proof to see what goes kaflooey. Following the Wikipedia description, every element of the disjoint union $X \sqcup Y$ unambiguously belongs to an "$X$-stopper" or to a "$Y$-stopper":

$$1_X \stackrel{i}{\mapsto} 2_Y \stackrel{j}{\mapsto} 3_X \stackrel{i}{\mapsto} \ldots$$

$$0_Y \stackrel{j}{\mapsto} 0_X \stackrel{i}{\mapsto} 1_Y \stackrel{j}{\mapsto} \ldots$$

But: when one attempts to define an isomorphism $\phi: X \to Y$ out of this by following the prescription, it immediately goes wrong. Look at what this putative function $\phi$ does to the "half-equal" elements $0_X$ and $1_X$. It sends them respectively to the not-at-all-equal elements $0_Y$ and $2_Y$. Thus it fails to respect

$$e_X(0_X, 1_X) \leq e_Y(\phi(0_X), \phi(1_X))$$

as required by law.

Answer 4

It is well-known that Grothendieck toposes and realizability toposes (for different reasons) are models of Intuitionistic Zermelo–Fraenkel set theory. Therefore both Andrej and Todd showed in their answers (in essentially different way) that Cantor–Bernstein–Schroeder cannot be proved in IZF.

Of course, this does not mean that Cantor–Bernstein–Schroeder property is incompatible with constructive mathematics --- it just shows that IZF is too weak to prove CBS. Therefore, a complementary question could be: what are the implications of IZF+CBS; does IZF+CBS make the logic collapse to the boolean case?

If I am not mistaken, the answer is no, and the counterexample is constructed below. However, I shall start with a negative observation.

Let $\Omega$ be a Heyting algebra with countable unions. An element $v \in \Omega$ is complementable if there exists an element $w \in \Omega$ such that $v \vee w = 1$ and $v \wedge w = 0$.

We say that $\Omega$ is a boolean algebra if its every element is a finite union of complementable elements (equivalently, if every element is complementable).

We say that $\Omega$ is a pro-boolean algebra if its every element is a countable union of complementable elements.

The claim is that every elementary topos with countable colimits satisfying Cantor–Bernstein–Schroeder propery is pro-boolean (i.e. its subobject classifier is a pro-boolean algebra).

Let $v \colon V \rightarrow 1$ be a "truth" value (a monomorphism into terminal object). We shall construct two objects $X = \coprod_{\mathbb{N}} 1$ and $Y = V \sqcup X$. There are obvious monomorphisms ${\iota_X}\colon{X}\rightarrow{Y}$ given by the coproduct injection, and ${v \sqcup \mathit{id}}\colon{Y}\rightarrow{X}$. Therefore, by Cantor–Bernstein–Schroeder there is an isomorphism ${b}\colon{Y}\rightarrow{X}$. Since coproducts in a topos are extensive, we may divide each component ${\iota_0}\colon V \rightarrow{Y}$, ${\iota_k}\colon 1 \rightarrow{Y}$ of the coproduct $Y$ along $b$ through coproduct's injections ${\iota_l} \colon 1 \rightarrow{X}$ obtaining elements $\alpha_{k,l}$ such that $Y \approx \coprod_k \coprod_l \alpha_{k,l} \approx \coprod_l \coprod_k \alpha_{k,l}$ and $b = \coprod_l b_l$ with each ${b_l}\colon{\coprod_l \alpha_{l,k}}\rightarrow{1}$ being an isomorphism (using again extensivity of coproducts and the fact that pullback of an iso is iso). Because unions in a topos are effective (and coproducts are disjoint) $1 \approx \coprod_l \alpha_{l,k} = \bigcup_l \alpha_{l,k}$ and so each $\alpha_{l,k}$ is complemented by $\bigcup_{x \neq l} \alpha_{x,k}$. Since every subterminal value can sit in exactly one way in the terminal object, $V = \bigcup_l \alpha_{l,0}$ is a countable disjoint union of complementable elements.

(We cannot get more from this construction; for example in the category of sheaves over rational numbers with the usual topology, $\coprod_{\mathbb{N}} 1 \approx V \sqcup \coprod_{\mathbb{N}} 1$ for (non-complementable) truth value $V$ corresponding to the open ball $(-1, 1)$; unfortunately there are other objects in this category that can serve as counterexamples for CBS. Let me also point that the standard procedure of constructing an isomorphism from two monomorphisms would not work in this case. However, by the above argument it is clear that such an isomorphism may be constructed for any pro-boolean topos. The solution is to not shift uniformly the whole $V$ (or its pseudocomplement), but to move each of (countably many) complementable parts of $V$ separately.)

---

[I am terribly sorry, now I see that there is an error in the following argument; I will try to fix it (on condition it is possible --- I am not sure now). I should have checked all relevant detail before posted this as an answer.]

For a positive result, consider set: $$\mathcal{D} = \lbrace 0, 1, \frac12, \frac13, \frac14, \dotsc\rbrace$$ with topology inherited from $\mathbb{R}$ and construct the category $\mathit{Sh}(\mathcal{D})$ of sheaves over $\mathcal{D}$. Every open set in $\mathcal{D}$ can be build from singletons $\lbrace\frac1n\rbrace$ and a set of the form $[0, \frac1k]$.

Let $F, G \colon \mathcal{D}^{op} \rightarrow \mathbf{Set}$ be any sheaves and assume there are monomorphisms $m \colon F \rightarrow G$ and $n \colon G \rightarrow F$. A monomorphism between sheaves is an injection on its each component, therefore by CBS theorem for sets $F(U) \approx G(U)$ for every open set $U$. Let $\phi_U \colon F(U) \approx G(U)$ be a collection of such isomorphisms. We shall construct an isomorphism $\alpha \colon F \rightarrow G$ between sheaves inductively:

• $\lambda_{[0, 1]} = \phi_{[0, 1]}$

• for every nonempty $F(\lbrace\frac1k\rbrace)$ choose an element $1_{\frac1k} \in F(\lbrace\frac1k\rbrace)$; if $F(\lbrace\frac1k\rbrace)$ is empty then $\lambda_{[0, \frac1{k+1}]} = \phi_{[0, \frac1{k+1}]}$, otherwise $\lambda_{[0, \frac1{k+1}]} = G([0, \frac1{k+1}] \subset [0, \frac1{k}]) \circ h_{\frac1k}$, where $h_{\frac1k} \colon F([0, \frac1{k+1}]) \rightarrow F([0, \frac1{k}])$ is the unique morphism to the product $F([0, \frac1{k}]) = F([0, \frac1{k+1}]) \times F(\lbrace\frac1k\rbrace)$ induced by $F([0, \frac1{k+1}]) \overset{!}\rightarrow 1 \overset{1_{\frac1k}}\rightarrow F(\lbrace\frac1k\rbrace)$ and the identity on $F([0, \frac1{k+1}])$

• similarly, for every nonempty $F([0, \frac1{k+1}])$ choose an element $1_{[0, \frac1{k+1}]} \in F([0, \frac1{k+1}])$; if $F([0, \frac1{k+1}])$ is empty then $\lambda_{\lbrace\frac1{k}\rbrace} = \phi_{\lbrace\frac1{k}\rbrace}$, otherwise $\lambda_{\lbrace\frac1{k}\rbrace} = G(\lbrace\frac1{k}\rbrace \subset [0, \frac1{k}]) \circ h_{{[0, \frac1{k+1}]}}$

• if $U$ is a disjoint union of the form $[0, \frac1k] \sqcup \bigcup_i\lbrace\frac{1}{n_i}\rbrace$, where $[0, \frac1k]$ is the largest interval contained in $U$, then $\lambda_{U} = \lambda_{[0, \frac1k]} \times \prod_i \lambda_{\lbrace\frac{1}{n_i}\rbrace}$, where the products are determined by structures of the sheaves.

In the second and third step we have chosen the components of $\lambda$ to be upward compatible, and in the fourth step the naturality condition follows from the universal property of products. Thus $F \approx G$.

[EDIT: Let me argue that $\phi_U$ may be chosen in such a way that each $\lambda_U$ is really an isomorphism. Assume, that all $F(\lbrace \frac1k\rbrace)$ are nonempty. Define $\mathit{colim}F([0, \frac1k])$ to be the colimit of the diagram: $$F([0, 1]) \rightarrow F([0, \frac12]) \rightarrow \cdots \rightarrow F([0, \frac1k]) \rightarrow \cdots $$ We have: $$(\mathit{colim}_kF([0, \frac1k])) \times (\prod_i F(\lbrace\frac1i\rbrace)) \approx F([0, 1]) \times \mathit{colim}\_k \prod\_{i > k} F(\lbrace\frac1i\rbrace) \approx F([0,1])$$ and similarly for $G$. Since in a locally presentable category monomorphisms are stable under directed colimits, both: $$\mathit{colim}F([0, \frac1k]) \overset{\mathit{colim}\left(m_{[0, \frac1k]}\right)}\rightarrow \mathit{colim}G([0, \frac1k])$$ and: $$\mathit{colim}F([0, \frac1k]) \overset{\mathit{colim}\left(n_{[0, \frac1k]}\right)}\leftarrow \mathit{colim}G([0, \frac1k])$$ are monomorphisms, thus by CBS for sets $\mathit{colim}F([0, \frac1k]) \overset{\phi_0}\approx \mathit{colim}G([0, \frac1k])$. Therefore, $\phi_{[0, 1]}$ may be assumed to be of the form $\phi_0 \times \prod \phi_{\lbrace\frac1k\rbrace}$. Likewise every $\phi_{[0, \frac1k]}$. ]

(BTW, I think we are not really that far from the inverse of the above theorem, but that is for another story...)

Answer 5

Failure of the law of the excluded middle is hard for me to imagine. But here is a try...

That König proof has this:

For any particular $a$, this sequence may terminate to the left or not

But perhaps we also have to consider the case of both: it terminates to the left and also does not terminate to the left... ???