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 😀
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.
Best Answer
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.