How strong is Cantor-Bernstein-Schröder?

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.