How strong is the Schröder–Bernstein theorem where one set is the natural numbers?

Question

The full Schröder–Bernstein theorem states that given an injection from A to B and also one from B to A, there is a bijection between A and B. It is equivalent to excluded middle, as shown in the paper Cantor–Bernstein implies Excluded Middle, arXiv:1904.09193 by Cécilia Pradic and Chad E. Brown, a result which has been formalized in at least two proof systems.

How strong is the theorem if we set A to the set of all natural numbers (and continue to allow B to be any set)? So far our best result is that given this case of Schröder–Bernstein plus the Limited Principle of Omniscience (LPO), we can prove excluded middle. There is an informal proof described here which has been formalized in metamath — to summarize it is a direct consequence of Lemma 3.2 from the Pradic–Brown paper ("Suppose that we have an omniscient set O and some sets A and B. If there exists a surjection f : O → A + B, then either A is inhabited or it is empty." where + is disjoint union).

Is a better result known? Also, is LPO→excluded middle equivalent to some better known principle, for example in the pantheon of LPO, LLPO, MP, etc.?

For the sake of concreteness, I'll ask with respect to a constructive set theory such as IZF, although my impression is that similar results hold in other foundations.

Answer 1

I have a slight strengthening of OP’s result. Assume the Schröder–Bernstein Theorem for $\mathbb{N}$.

Lemma (Creating Subject): for all propositions $P$, there exists a function $f : \mathbb{N} \to \{0, 1\}$ such that $P \iff \exists n (f(n) = 1)$.

Proof: let $S = \{n \in \mathbb{N} \mid n > 1 \lor P\}$. Let $g \colon \mathbb{N} \to S$ be a bijection, which exists by Schröder–Bernstein for $\mathbb{N}$. Define $$ f(n) = \begin{cases} 1 & g(n) = 1 \\ 0 & \text{otherwise.} \end{cases} $$ Then there is some $n$ such that $f(n) = 1$, iff there is some $n$ such that $g(n) = 1$, iff $1 \in S$, iff $P$. $\square$

Under countable choice, the above lemma is actually equivalent to Schröder–Bernstein for $\mathbb{N}$.

Now assume Markov’s Principle, and assume $\neg \neg P$. Take $f$ as in the above lemma. Then we have $\neg \neg \exists n (f(n) = 1)$. By Markov’s Principle, $\exists n (f(n) = 1)$. Therefore, $P$.

So under Markov’s Principle, Schröder–Bernstein for $\mathbb{N}$ is equivalent to full excluded middle. Since Markov’s Principle is strictly weaker than the Limited Principle of Omniscience, this is a slight strengthening of OP’s result. It also explains Hanul Jeon’s note that Schröder–Bernstein doesn’t hold in the effective topos, since in that topos, LEM fails but MP holds.

Finally, note that my Lemma is one axiomatization of the “Creating Subject” (see Intuitionism in the Philosophy of Mathematics at SEP, sections 2.2 and 5.4 for a good summary), so I’m sure that there are those who have studied this problem in more detail. Assuming countable choice for sequences, the Creating Subject Lemma implies Schröder–Bernstein for $\mathbb{N}$. To demonstrate this, consider the following theorem:

Theorem: Schröder–Bernstein for $\mathbb{N}$ is equivalent to the following. For all predicates $P$ on $\mathbb{N}$, there exists a function $g \colon \mathbb{N}^2 \to \{0, 1\}$ such that for all $n$, $P(n) \iff \exists m (g(n, m) = 1)$.

Proof: suppose Schröder–Bernstein for $\mathbb{N}$, and let $S = \{n \in \mathbb{N} \mid n \text{ odd } \lor P(n/2)\}$. Let $h \colon \mathbb{N} \to S$ be a bijection, which exists by Schröder–Bernstein. Define $$ g(n, m) = \begin{cases} 1 & h(m) = 2n \\ 0 & \text{otherwise.} \end{cases} $$ Then $g$ has the required property.

Now suppose for all $P$, there exists $g$ as in the theorem. Consider some subset $S \subseteq \mathbb{N}$ with injection $\mathbb{N} \to S$. Take some $g$ such that for all $n$, $n \in S \iff \exists m (g(n, m) = 1)$. Let $w \colon \mathbb{N} \to \mathbb{N}^2$ be a bijection and $w(n) = (w_1(n), w_2(n))$. Define $h \colon \mathbb{N} \to S$ recursively by letting $h(n) = w_1(m)$, where $m$ is the smallest natural number such that $g(w(m)) = 1$ and $w_1(m) \notin \{h(j) \mid j < n\}$. Then $h$ is a well-defined because $S$ is constructively infinite, and $h$ is a bijection. $\square$

Under countable choice for sequences, the Creating Subject Lemma thus implies Schröder–Bernstein for $\mathbb{N}$. Thus, I recommend seeking out literature on the Creating Subject axioms to study your theorem. There is a fair amount of Brouwerian philosophy discussing the Creating Subject if that is your cup of tea, and I am sure there is plenty of mathematics done on this subject as well.