SSequence said:
Either we show:
(1) ##\forall x \in S \,\, [\,\exists r \in \mathbb{R} \,\,( \, r \notin x \, )\,] ##
OR we show:
(2) ##\lnot \, \exists x \in S \,\, [ \,\, \forall r \in \mathbb{R} \,\,( \, r \in x \, ) \,\, ] ##
Neither of these are the final thing we want to prove. However, writing down the final thing we want to prove in logical notation (which I will do below) does make clearer the point I think you are trying to make.
First, a technical point: we are
not talking about the set ##\mathbb{R}##. We are talking about the set of infinite strings of binary digits, which I will call ##\mathbb{B}##. Proving that there is a bijection between ##\mathbb{B}## and ##\mathbb{R}## is a
separate theorem (and one which, as I have noted earlier in this thread, Cantor himself did
not prove).
Second, another technical point: we have been talking about sequences of infinite strings of binary digits, but any such sequence is equivalent to a function from ##\mathbb{N}##, the set of natural numbers, to ##\mathbb{B}##. And viewing it as a function makes the logical notation nicer, so I'll do that below.
Given that, the correct statement of the theorem that I have called Phase 1 is:
##\forall f: \mathbb{N} \to \mathbb{B} \, \left[ \, \exists b \in \mathbb{B} \, \left[ \, \lnot \, \exists n \in \mathbb{N} \, \left( \, f(n) = b \, \right) \, \right] \, \right]##
In other words, given a function ##f: \mathbb{N} \to \mathbb{B}##, we can always find an infinite binary string ##b## such that there is no natural number ##n## that is mapped to ##b## by the function ##f##. We can find this string by using Cantor's diagonal construction. There is no proof by contradiction involved, because we never made any
assumption regarding whether or not there were any infinite binary strings that were not the results of ##f## for any natural number. No such assumption is required for there to exist a function ##f: \mathbb{N} \to \mathbb{B}##.
The final thing we want to prove (the conclusion of what I have called Phase 2) is:
##\lnot \exists f: \mathbb{N} \to \mathbb{B} \, \left[ \, \forall b \in \mathbb{B} \, \left[ \, \exists n \in \mathbb{N} \, \left( \, f(n) = b \, \right) \, \right] \, \right]##
In other words, there does not exist any function ##f: \mathbb{N} \to \mathbb{B}## which is surjective, i.e., which has every element of ##\mathbb{B}## as its result for some element of ##\mathbb{N}##.
Now, you are correct that this can be obtained from the Phase 1 conclusion above by simple quantifier transformations, so it is actually logically equivalent to the Phase 1 conclusion. And I would say that, if you want to take that position, then you are taking the position that
no proof by contradiction is required
anywhere in the argument--at least not if we use Cantor's diagonal construction. If we use Cantor's diagonal construction, we are following the line of proof described above, which, as I noted above, does
not require assuming that ##f## is surjective. The fact that ##f## cannot be surjective does come out as a conclusion of the argument, but that does
not mean we had to put in its negation as an
assumption to the argument. We didn't.
On this view, what I described as Phase 2 of the argument is simply recognizing this logical equivalence--i.e., recognizing that, as soon as you have proved Phase 1, you already have enough, logically, to prove Phase 2, because it's just a matter of working out the logical equivalence of the two statements. I suppose you could argue that part of that recognition process is going to involve viewing the working out of the logical equivalence as a sort of proof by contradiction. But I don't see it that way. Even if you were to construct a formal "proof" that involved the extra assumption that ##f## was surjective as its starting point, the logical equivalence above guarantees that you would be able to eliminate that initial assumption and still maintain the proof's validity.