8
$\begingroup$

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.

$\endgroup$
9
  • 2
    $\begingroup$ 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/… $\endgroup$ Dec 19, 2012 at 14:25
  • 2
    $\begingroup$ 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. $\endgroup$ Dec 19, 2012 at 14:47
  • $\begingroup$ The constructibility theories include global choice, but I am looking at things like $\mathsf{B}_0^\mathrm{set}$ or $\mathsf{ATR}_0^\mathrm{set}$. $\endgroup$ Dec 19, 2012 at 14:51
  • $\begingroup$ $\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. $\endgroup$ Dec 19, 2012 at 15:19
  • $\begingroup$ 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. $\endgroup$ Dec 19, 2012 at 15:48

2 Answers 2

6
$\begingroup$

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

$\endgroup$
0
$\begingroup$

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

$\endgroup$
2
  • $\begingroup$ I've fixed an oddly-behaving link. $\endgroup$ Jan 28, 2021 at 18:00
  • $\begingroup$ Those links were not mine, though I am glad they were added (and work properly now). $\endgroup$ Jan 28, 2021 at 18:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.