# What is the status of Cantor-Schroder-Bernstein in Reverse Math?

I'd like to know which of the set theories in SOSOA prove what versions of Cantor-Schroder-Bernstein? For my own purposes I can use arbitrarily high quantifier complexity, but I wonder how little transfinite recursion will suffice.

-
Could you clarify a bit what set theories you mean? There aren't that many proper set theories in SOSOA and the way Simpson approaches things, they usually implicitly include global choice or that every set is countable, both of which make CSB rather trivial. For other weak set theories, this old answer of mine is relevant - mathoverflow.net/questions/18042/… –  François G. Dorais Dec 19 '12 at 14:25
Meanwhile, the computable version of the Cantor-Schroeder-Bernstein theorem is known as Myhill's theorem en.wikipedia.org/wiki/Myhill_isomorphism_theorem, and the proof relativizes to oracles. –  Joel David Hamkins Dec 19 '12 at 14:47
The constructibility theories include global choice, but I am looking at things like $\mathsf{B}_0^\mathrm{set}$ or $\mathsf{ATR}_0^\mathrm{set}$. –  Colin McLarty Dec 19 '12 at 14:51
$\mathsf{ATR}_0^{\mathrm{set}}$ includes the Axiom of Countability. $\mathsf{B}_0^{\mathrm{set}}$ is extremely weak and very hard to use; that doesn't seem to fit well with the second part of your question. –  François G. Dorais Dec 19 '12 at 15:19
If countablity is necessary to to prove CSB in $\mathsf{ATR}_0^{\mathrm{set}}$, that would help me know how to direct my efforts. And $\mathsf{B}_0^{\mathrm{set}}$ supports a considerable theory of ordinals. It might prove enough of CSB for me. This is for work in progress and I do not know `how much' of CSB I would need. For now, I wonder what versions of it are available. –  Colin McLarty Dec 19 '12 at 15:48

I will show that variants of the following proof work in extremely weak set theories but perhaps not in $\mathsf{B}_0^{\mathrm{set}}$.

We can always reduce to the case where one of the two injections is an inclusion. Suppose that $B \subseteq A$ and $f:A \to B$ is an injection. Say that $x \in B$ is a $B$-stopper if there is a finite sequence $\langle x_0,\dots,x_n \rangle$ with $x_0 = x$, $x_n \in B - f[A]$, and $f(x_{i+1}) = x_i$ for each $i \lt n$. The function $g:A \to B$ defined by $g(x) = x$ if $x$ is a $B$-stopper and $g(x) = f(x)$ if $x$ is not a $B$-stopper is a bijection.

The verification that $g$ is a bijection is a straightforward feat of plain logic provided that the base theory can handle the formation of arbitrary finite sequences. (I won't consider systems that can't handle arbitrary finite sequences.) So it is enough to make sure that $g$ exists. Assuming $\Delta_0$-comprehension, this is equivalent to the existence of the set of $B$-stoppers. If $B^{\lt\omega}$ exists, then the set of $B$-stoppers can be formed by $\Delta_0$-comprehension.

Sadly, Simpson's system $\mathsf{B}_0^{\mathrm{set}}$ does satisfy $\Delta_0$-comprehension, but it does not prove that $X^{\lt\omega}$ exists for every set $X$. In fact, I don't think it is known whether this system proves that $X^n$ exists for every set $X$ and every $n \lt \omega$. (See A. R. D. Mathias, Weak systems of Gandy, Jensen and Devlin, where this system is known as $\mathsf{GJI}_0$, modulo the fact that Simpson's formulation of the axiom of infinity is a little unusual. I think Simpson's axiom of infinity prevents Gandy's model but not the general problem it illustrates.)

If $B^{\lt\omega}$ does not exist, then the definition of $B$-stopper given above requires $\Sigma_1$-comprehension. However, the precise set of $B$-stoppers is not needed. If $C \subseteq B$ is such that $B-f[A] \subseteq C$ and both $C$ and $A-C$ are closed under $f$, then the map $h:A\to B$ defined by $h(x) = x$ if $x \in C$ and $h(x) = f(x)$ if $x \in A-C$ is a bijection. Over $\mathsf{B}_0^{\mathrm{set}}$ (even without infinity), the existence of such a set $C$ is easily established using the compactness theorem for propositional logic, which is known to be weaker than $\Sigma_1$-comprehension. This is the weakest system that I know which proves CSB.

Remark. The language of propositional logic is difficult to work with in set theories that do not prove that $X^{\lt\omega}$ exists for every set $X$. However, the theory in question consists of $p_x \leftrightarrow p_{f(x)}$ for $x \in A$, $p_x$ for $x \in B-f[A]$, $\lnot p_x$ for $x \in A-B$. Since these formulas are all short, we can get by with standard finite powers of sets.

In any case, I strongly advise against working in set theories that cannot prove that $X^{\lt\omega}$ exists for every set $X$.

-