set theory - Axiom of Infinity needed in Cantor-Bernstein?

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.

• Next tag removed - Generalizations of "standard" calculus
• Previous soft question - A single paper everyone should read?