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

Question

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.

Answer 1

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$.

Answer 2

The papers [1b, 2] answer your question for the Cantor-Bernstein theorem (CBN) for $\mathbb{N}$, working in Kohlenbach's higher-order Reverse Mathematics ([0]). As is customary, sets are defined via characteristic functions (see e.g. [1]). In this case, CBN is hard to prove as follows.

The principle CBN is formulated in [2] in third-order arithmetic as follows:

let $A \subset \mathbb{R}$ be such that there exists $F:\mathbb{R}\rightarrow \mathbb{N} $ injective on $A$ and injective $G:\mathbb{N} \rightarrow\mathbb{R}$ such that $(\forall a\in A)(\exists n\in \mathbb{N})(G(n)=a)$. Then there is $H:\mathbb{R} \rightarrow\mathbb{N}$ such that $H$ is injective on $A$ and surjective, i.e. $(\forall n\in \mathbb{N})(\exists a\in A)(H(a)=n)$.

Then CBN cannot be proved in Z$_2^\omega+$ QF-AC$^{0,1}$, a conservative extension of Z$_2$ with third-order comprehension functionals S$_k^2$ for $\Pi_k^1$-formulas in L$_2$.

Dag Normann and I are have explored CBN in more detail in [1b], as follows:

On one hand, a slight extension of CBN already yields the 'explosive' principle cocode$_0$ from [2]; the latter yields $\Pi_2^1$-comprehension when combined with the Sulsin functional, i.e. higher-order $\Pi_1^1$-comprehension.

On the other hand, Z$_2^\omega$ + CBN cannot prove NBI, where the latter expresses that there is no bijection from $[0,1]$ to $\mathbb{N}$.

References

[0] Kohlenbach, U., Higher order reverse mathematics, Reverse mathematics 2001, Lect. Notes Log., vol. 21, ASL, 2005, pp. 281–295. doi:10.1017/9781316755846.018, BRICS preprint

[1] Kreuzer, A., Measure theory and higher order arithmetic, Proc. Amer. Math. Soc. 143 (2015), no. 12, 5411–5425, doi:10.1090/proc/12671, arXiv:1312.1531

[1b] D. Normann and S. Sanders, On robust theorems due to Bolzano, Weierstrass, and Cantor in Reverse Mathematics, 2021 https://arxiv.org/abs/2102.04787

[2] S. Sanders, Countable sets versus sets that are countable, arXiv:2011.01772