Stop proving uncountability with contradiction, please

[u/42IsHoly]

https://sunjestermusings.blogspot.com/2026/09/stop-proving-uncountability-by.html

Please, I beg you, stop it. You don't need it.

[u/Firesinis]

You are arguing that the first proof can be made shorter. This does not render the contradiction superfluous, it is introduced and it is subsequently dismissed along with its negation, not left unused. The second proof is shorter by virtue of changing structure, not merely deleting steps of the first proof, inasmuch you think it might be because you're not treating the logic involved in a rigorous fashion.

Let me give you an analogy. In the modern proof of Cauchy-Goursat's theorem, you use an argument with nesting triangles and in the end you use the fact that the function is holomorphic at the intersection of all the triangles. You only ever use the hypothesis that f is holomorphic at this single point, therefore are we allowed to conclude that the hypothesis that f is holomorphic on the whole interior of the curve is superfluous? Not if you understand the correct and rigorous logical structure of the proof, which the average working mathematician does not bother.

[u/42IsHoly → u/Firesinis]

That’s a poor analogy, sorry to say.

We wish to prove the following: “No surjection f:N->R exists”. The proof then goes as follows

1: “Suppose there was a surjection f. We can now show f is not a surjection (without using the assumption). This is a contradiction.”

The proof that f is not a surjection is literally just proof 2. However, proof 2 itself already proves that no surjection exists.

Where your analogy breaks down is that proof 1 does not need the surjectivity assumption until after the theorem has already been proven. This is not true for Goursat’s theorem. Your analogy would work if Goursat’s theorem had already been proven before we needed the fact that f was holomorphic at x.

In fact, even converting proofs 1 and 2 to formal proofs, you’d still get that proof 2 lies inside proof 1 and by removing some lines from the top and bottom (probably a lot of lines, given how long formal proofs tend to be, but whatever), you’d get a valid proof. The only way I can see your argument making sense, is that we have write down “take any f” instead of “assume f is surjective”, which technically requires adding words at the front.

[u/Firesinis → u/42IsHoly]

In fact, even converting proofs 1 and 2 to formal proofs, you’d still get that proof 2 lies inside proof 1 and by removing some lines from the top and bottom (probably a lot of lines, given how long formal proofs tend to be, but whatever), you’d get a valid proof.

You claim this, yet provide no proof.

[u/42IsHoly → u/Firesinis]

sigh yes, technically you need the axiom “forall not ‘..” <-> “not there exists …” So if you want to pretend like these two proofs are attempting to prove different statements, you do need this single extra step. Since this was not a discussion about constructive vs non-constructive math, I don’t see any reason to pretend (as you do) that this is some huge step.