Axiom of Infinity needed in Cantor-Bernstein? - MathOverflow

Axiom of Infinity needed in Cantor-Bernstein?

2010-03-13T07:35:32Z

Can one prove the Cantor-Bernstein (or Schröder-Bernstein) theorem without using the Axiom of Infinity?

Answer by Robin Chapman for Axiom of Infinity needed in Cantor-Bernstein?

2010-03-13T08:05:39Z

One of the standard proofs avoids the Axiom of Infinity. It's based on the Tarski fixed-point theorem, see for instance www.cs.ucla.edu/~palsberg/course/cs232/papers/bernstein.pdf . But it does use the Power Set Axiom in an essential way.

Answer by Andrej Bauer for Axiom of Infinity needed in Cantor-Bernstein?

2010-03-13T08:08:10Z

Yes, there is a way to prove Cantor-Bernstein theorem from Tarski's fixed point theorem, see a proof outline on MathWorld.

Answer by Joel David Hamkins for Axiom of Infinity needed in Cantor-Bernstein?

2010-03-13T17:55:04Z

(I also like the fixed-point proof mentioned by Andrej and Robin, and indeed, this is the proof I usually use of this theorem. But I claim that there is another more general way to answer the question.)

My answer is that any of the standard proofs can be transformed into a proof not using the Infinity axiom as an assumption. The reason is that if Infinity fails, then every set is finite, and in this case, the Cantor-Schroeder-Bernstein statement becomes trivial---it's just the pigeonhole principle that if n ≤ m ≤ n for natural numbers, then n = m.

So, take any proof of CSB using Infinity and make a new argument omitting that assumption, by simply splitting into cases. Case 1, if Infinity holds, use the original argument. Case 2, if Infinity fails, then CSB becomes trivial.

For this reason, I find the question perhaps to be somewhat odd. The power and usefulness of the Cantor-Schroeder-Bernstein theorem seems to lay largely in the case when there ARE infinitely sets, and is trivialized when there are none.

Answer by François G. Dorais for Axiom of Infinity needed in Cantor-Bernstein?

2010-03-15T14:08:27Z

Actually, the usual proof of the Cantor-Schröder-Bernstein Theorem does not use the Axiom of Infinity (nor the Axiom of Powersets).

By the usual proof, I mean the one found on Wikipedia, for example. Using the notation from that proof, the main point of contention is whether we can form the sets $C_n$ and $C = \bigcup_{n=0}^\infty C_n$. These sets exist by comprehension:

$C_0 = \{x \in A: \forall y \in B\,(x \neq g(y))\}$

$C_n = \{x \in A: \exists s\,(s:\{0,\dots,n\}\to A \land s(0) \in C_0 \land (\forall i < n)(s(i+1) = g(f(s(i)))) \land s(n) = x\}$ ,

where abbreviations such as $s:\{0,\dots,n\}\to A$ should be replaced by the equivalent (bounded) formulas in the language of set theory. The definition of $C_n$ is uniform in $n$, and so

$C = \{x \in A: \exists n\,(\mathrm{FinOrd}(n) \land x \in C_n)\}$ ,

where $x \in C_n$ should be replaced by the above definition and $\mathrm{FinOrd}(n)$ is an abbreviation for "$n$ is zero or a successor ordinal and every element of $n$ is zero or a successor ordinal." An alternate definition of $C$ is

$C = \{x \in A: \forall D\,(C_0 \subseteq D \subseteq A \land g[f[D]] \subseteq D \to x \in D)\}$ ,

which shows that $C$ is $\Delta_1$-definable. The rest of the proof uses induction on finite ordinals, but since the definition of the sets $C_n$ is uniform these are special cases of transfinite induction.

In conclusion, it looks like the proof could work in Kripke-Platek Set Theory — which has neither the Axiom of Infinity nor the Axiom of Powersets — provided that the two definitions of $C$ given above are provably equivalent. I haven't tried to check whether the two definitions are provably equivalent but, in any case, the proof can be carried out in Kripke-Platek Set Theory with $\Sigma_1$-Comprehension.