How strong is Cantor-Bernstein-Schröder?

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.

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.

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.

• I need to look at the standard proofs of Myhill's theorem, but I will bet that the constructive version would use Markov principle and/or countable choice. Note that the theorem stated constructively will be about $\lnot\lnot$-stable subsets of $\mathbb{N}$. – Andrej Bauer Dec 11 '15 at 18:59

The paper Cantor-Bernstein implies Excluded Middle by Pierre 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.

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.

• I find this line of reasoning a bit misleading. You have observed that there are two models of constructive mathematics in which CBS is false. From this you cannot conclude that CBS has "no constructively true" version, unless you also believe that constructive mathematics requires all functions to be continuous, or at least that there be no discontinuous ones. That is a rather commited kind of constructivism, indeed a very Dutch one :-) – Andrej Bauer Dec 26 '16 at 22:22
• An actual question is this: does CBS imply existence of discontinuous functions? How badly discontinuous must they be? – Andrej Bauer Dec 26 '16 at 22:23
• There can be no discontinuous total function on spreads in constructive math. This is not a 'rather committed' or 'Dutch' kind of constructivism, but a simple consequence of the ubiquitous Brouwerian counterexamples which demonstrate that any partial function which is discontinuous cannot be claimed to be total. Bishop must have given many such examples. – Frank'a Waaldijk Dec 27 '16 at 9:19
• I think we're using the word "constructive" differently. I use it in Bishop's sense, so that constructive mathematics is fully compatible with classical mathematics as well as Brouwerian intuitionism. Under this understanding, there can be discontinuous functions, namely in classical mathematics. So constructive mathematics is compatible with existence of discontinuous functions. I suspect your constructivism is more of a constructivism. – Andrej Bauer Dec 27 '16 at 9:43
• Both in INT and RUSS, total functions on complete metric spaces are continuous. From this one easily sees that $\neg$CBS is a theorem, since for instance the closed disc $D$ in $\mathbb{R}^2$ can be embedded in the the punctured closed disc $D'$ (with the origin removed) and vice versa, but there can be no bicontinuous bijection between the two. – Frank'a Waaldijk Mar 3 '17 at 14:58

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.

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.

• Can you give an example of such an example? – Andrej Bauer Dec 27 '16 at 9:47
• Interesting! If I am not mistaken, CBS with the decidability assumptions that you propose must be equivalent to a version formulated towards the end of the question ($A\sqcup A_1\sqcup A_2\cong A$ implies $A\sqcup A_1\cong A$). If it is so, can you provide a proof of it in this form? – მამუკა ჯიბლაძე Dec 27 '16 at 10:02
• Well, all examples I'm aware of establish bijections between countable sets. Let me give just one simple example: $\mathbb{N} \leftrightarrow \mathbb{N} \times \mathbb{N}$, $x \mapsto (0,x)$, $(x,y) \mapsto 2^x * 3^y$. Of course, you can prove this by constructing an explicit bijection, but this constructive CBS might be easier to apply. – Valery Isaev Dec 27 '16 at 10:07
• Regarding $A \amalg A_1 \amalg A_2 \cong A \amalg A_1 \amalg A_2 \cong A$ implies $A \amalg A_1 \cong A$. I don't think it is possible to apply this theorem to this preoblem. It is easy to define embeddings with decidable images, but the other condition might not hold. Actually, this condition is the most difficult to fulfill. Usually, I try to define embeddings so that this subset is empty. Regarding your question, it seems impossible to control this subset. – Valery Isaev Dec 27 '16 at 10:35