Where exactly does this proof of Schroder Bernstein use the law of the excluded middle?

Question

I have finally worked my way through the entirety of this proof of the Schröder Bernstein Theorem but have now learned something new about it while browsing Stack Exchange - that one has to use the law of the excluded middle to prove Schröder Bernstein. Where exactly does this proof use the law of excluded middle? I can't see it - my guess would be that the author is using it somewhere around step (1), but I'm not quite sure. Also, since I don't really have a strong background in logic, it would be fantastic if someone could explain to me why the law of excluded middle is necessary for Schröder Bernstein. Thanks!

Answer 1

It is in the line

Next, we can represent $S$ as $$S = (S \setminus S_1) \cup (S_1 \setminus S_2) \cup \cdots \cup (S_k \setminus S_{k + 1}) \cup \cdots \cup D$$

Every other line of the proof works without excluded middle, but this one doesn’t. In particular, you’d have to be able to decide, for each $x \in S$, whether $x \in S_1$ or not. This is not possible in general without excluded middle.

Answer 2

To address Alberto Takase's interesting question, there is a paper by Pradic and Brown that answers it in the affirmative, that Cantor-Bernstein does indeed necessitate excluded middle. As excluded middle is independent from IZF, where the authors' argumentation takes place, this entails that all arguments proving it in the language of Zermelo Fraenkel have to be strictly classical—in particular, the proof you cite in the ProofWiki has to certainly use it somewhere (the place Mark Saving has pointed out is it). It is a relatively short and elementary read, though I find it to still be a bit difficult for beginners in constructive logic, or even logic in general, yet it makes up for the difficulty by being as fruitful for such a reader given that they truly understand the material.