How strong is Cantor-Bernstein-Schröder?

Question

There are several questions here on MO about the Cantor-Bernstein-Schröder ((C)BS) theorem, but I could not find answers to what arose to me recently.

Although I don't think I need to recall it here, the theorem states that if there are embeddings $i:A\hookrightarrow B$, $j:B\hookrightarrow A$ then there is a bijection between $A$ and $B$.

First question -

As explained in several answers to one of those questions, CBS is not constructively valid. Does validity of CBS actually imply excluded middle? If not - does CBS imply any nontrivial (say, not intuitionistically valid) propositional sentence?

Some motivation comes from Diaconescu's theorem that the Axiom of Choice implies excluded middle. Again, as mentioned in several of the answers to the above questions validity of CBS does not require choice, but this does not exclude the possibility that, say, the propositional part of some form of constructive set theory + CBS is strictly stronger than "mere" intuitionism. Btw, the Wikipedia article that I linked to for Diaconescu's theorem mentions that it is in a form of a Problem (Problem 2 on page 58) in Bishop's "Foundations of constructive analysis". What is said there literally is "Construct a surjection which is not onto", and the whole set of problems has an instruction saying that the not has to be understood in the sense of discussion at the end of Section 2. What is said in that discussion seems to indicate that one has to work in intuitionistic logic although I am not sure.

I mention all this to illustrate that there might be some subtle points involved. Anyway, here is my

Second question -

Is there a constructively valid statement that becomes equivalent to CBS under excluded middle?

Again, it might be not obvious what is precise sense of this, but let me give another piece of motivation. One might replace $B$ with $j(B)\subseteq A$, then CBS becomes equivalent to the following:

Given an injective self-map $e:A\hookrightarrow A$, for any $e(A)\subseteq A'\subseteq A$ there is a bijection between $A$ and $A'$.

Now recall that Lawvere's notion of the object of natural numbers (NNO) can be equivalently given as the initial algebra for the functor $A^+:=A\sqcup 1$. That is, the NNO is characterized up to isomorphism as an object $N$ equipped with a map $N^+\to N$ and initial among objects with such structure. By Lambek's lemma it then follows that this $N^+\to N$ is an isomorphism. It can be also shown that if $A^+\to A$ is mono then the induced map $N\to A$ is mono too.

In view of this and of the above reformulation of CBS it is natural to ask what happens if one replaces 1 with some other object $T$. Similarly to the above statement in bold, if there is a mono $A\sqcup T\rightarrowtail A$ then $A$ will contain a copy of the initial $\_\sqcup T$-algebra, in particular, a subobject $I\rightarrowtail A$ with $I\sqcup T$ isomorphic to $I$.

The latter somehow suggests a form of the above equivalent of CBS with complemented "remainder". Still the formulation escapes me although I have very strong feeling there must be something precise behind it. And although at the first glance this looks like an uninspiring weakening, the example of the NNO shows it might be interesting: $0:1\to N$ is a complemented element more or less by definition, but this does not make the notion of NNO too weak.

I realize all this does not add much clarity to the second question, but then if it would be clear to me I would not need to ask :D

Slightly later

Inspired by the mentions of decidability in Andrej Bauer's answer, here is a sketch of one candidate: I find it quite plausible that constructively $A\sqcup A_1\sqcup A_2\cong A$ implies $A\sqcup A_1\cong A$. Is it so? In case it is, can one do better? That is, is there a still constructively valid statement obviously implying the above but not obviously equivalent to it? Somehow I feel there must also be a "less complemented" version...

...and later - Ingo Blechschmidt commented with a link to an n-category café entry which in turn had a link to "Theme and variations: Schroeder-Bernstein" at the Secret Blogging Seminar; seems to be related, although I cannot find answers to the above questions there.

Answer 1

The paper Cantor-Bernstein implies Excluded Middle by Cécilia Pradic and Chad E. Brown shows that Excluded Middle is equivalent to CBS in constructive set theory.

I don't understand Toposes very well, but I believe the same proof goes through in a Topos with NNO.

Answer 2

I do not know how to answer your questions, but here are some remarks that should make you worried.

First, in the realizability topos over infinite-time Turing machines there is a mono $\mathbb{N}^\mathbb{N} \to \mathbb{N}$, see this paper. Since there is of course a mono in the other direction, this implies that any kind of constructive CBS must exclude this counter-example.

One would hope, for instance, that it is possible to get a constructive CBS by assuming that the sets in question have decidable equality. Alas, this will not do because in the effective topos there is a subset $S \subseteq \mathbb{N}$ which is not enumerable. Then the set $T = \{2 n \mid n \in S\} \cup \{2 n + 1 \mid n \in \mathbb{N}\}$ has decidable equality, and there are injections between $T$ and $\mathbb{N}$, however $T$ is not enumerable, or else $S$ would be as well. Thus $T$ cannot be isomorphic to $\mathbb{N}$.

Good luck finding a constructive CBS.

Answer 3

The Myhill isomorphism theorem is often taken as a computability-theoretic version of the Cantor-Schroder-Bernstein theorem, and this can be interpreted as a version of the result for constructive logic.

Answer 4

Elephant D 4.1, Lemma 4.1.12 (p. 951):

Let $\mathscr E$ be a topos with a natural number object N. If the Cantor-Bernstein theorem holds in $\mathscr E$, then every subobject of an object of $\mathscr E$ is an N-indexed union of complemented subobjects.

In "Thoughts on the Cantor-Bernstein Theorem" by B. Banaschewski & G. C. L. Brümmer (Quaestiones Math. 9 1986 1-27), it is proved that in a topos with a NNO, excluded middle is implied by the following strengthening of the CBS (which they call CBT): for monomorphisms $f:A\to B$, $g:B\to A$ there is an isomorphism $h:A\to B$ with its graph contained in the relation $f\cup g^{-1}$.

Both sources contain different examples of non-Boolean toposes where CBS and even CBT holds, as well as one where CBS holds and CBT fails.

Answer 5

The Cantor-Schröder-Bernstein theorem (CBS) implies excluded middle in intuitionistic mathematics (INT) and in recursive mathematics (RUSS), since CBS is false ($\neg$CBS is a theorem), and ex falso quodlibet...also excluded middle. The reason for this is that both in INT and RUSS, total functions on spreads are continuous. In classical math CBS doesn't hold for continuous functions either for the same reason.

This continuity aspect of total functions cannot be avoided in constructive math, therefore there are no constructively true versions of CBS in any general sense.

Answer 6

If you look carefully into the proof of CBS theorem, you might notice that LEM is used in few places there. You can explicitly assume these usages in the statement of the theorem. So, if you assume that embeddings have decidable images and also a certain subset of one of the sets (the intersection of $\mathrm{im}((j \circ i)^n)$ for all $n$) is also decidable, then CBS becomes valid constructively, and under LEM it is equivalent to the usual CBS. Though this observation is quite trivial, it is useful in practive since sometimes these subsets are decidable, so we can actually apply this constructive version of CBS.