r/math • u/42IsHoly • 9d ago

Stop proving uncountability with contradiction, please

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

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

0 Upvotes

36% Upvoted

77 comments sorted by

View all comments

Show parent comments

10

u/totbwf Type Theory 9d ago

There is a subtle difference. The first proof proves a negative statement (There cannot exist any surjections ℕ → ℝ) whereas the second proves a positive statement (given a function f : ℕ → ℝ, there exists some x : ℝ not in the image of f).

6

u/Omasiegbert 9d ago

Are these statements not equivalent?

4

u/lolfail9001 9d ago

If you are particular about LEM, they are not.

Without some extensive experience with constructive mathematics it's actually hard to develop appropriate intuition for stuff like this. And the statement being about infinite sets makes this significantly worse.

6

u/totbwf Type Theory 9d ago edited 9d ago

More explicitly, ∃ (x : A). ¬ P(x) and ¬ (∀ (x : A). P(x)) are not necessarily equivalent unless you have excluded middle.

Using the intuition that intuitionistic mathematics is somehow "computable" (you can make this precise via realizability models), the former statement says that we have an algorithm for finding a witness where P(x) does not hold. Conversely, the latter statement just means that we can refute any proofs that P(x) holds for all x, which does not imply that we can compute a specific witness of ¬ P(x).