What is the status of Cantor-Schroder-Bernstein in Reverse Math? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T14:37:09Z http://mathoverflow.net/feeds/question/116788 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/116788/what-is-the-status-of-cantor-schroder-bernstein-in-reverse-math What is the status of Cantor-Schroder-Bernstein in Reverse Math? Colin McLarty 2012-12-19T13:58:48Z 2012-12-19T20:26:22Z <p>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.</p> http://mathoverflow.net/questions/116788/what-is-the-status-of-cantor-schroder-bernstein-in-reverse-math/116813#116813 Answer by François G. Dorais for What is the status of Cantor-Schroder-Bernstein in Reverse Math? François G. Dorais 2012-12-19T19:53:35Z 2012-12-19T20:26:22Z <p>I will show that variants of the following proof work in extremely weak set theories but perhaps not in $\mathsf{B}_0^{\mathrm{set}}$.</p> <blockquote> <p>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.</p> </blockquote> <p>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.</p> <p>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, <a href="https://www.dpmms.cam.ac.uk/~ardm/weaksystems.pdf" rel="nofollow"><em>Weak systems of Gandy, Jensen and Devlin</em></a>, 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.)</p> <p>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.</p> <p><em>Remark.</em> 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.</p> <p><em>In any case, I strongly advise against working in set theories that cannot prove that $X^{\lt\omega}$ exists for every set $X$.</em></p>