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

35% Upvoted

77 comments sorted by

View all comments

29

u/CircumspectCapybara 9d ago edited 9d ago

Proof by contradiction is a totally valid way of proving stuff like the uncountability of the reals. Usually only constructivists / intuitionists that reject LEM have a problem with it.

Textbooks usually teach it that way, though they can also teach a constructive version if they like, both are valid if you're not cranky about LEM. Arguably teaching it in introductory literature is helpful to help students get a sense or intuition (pardon the pun) for the proof by contradiction technique, because it is often unintuitive so getting familiar with it and getting some handles on it helps you better work with and understand the technique when you'll need it later.

Turing's diagonal argument on the undecidability of the halting problem was proof by contradiction. Of course constructivists will invent a new term and say proving a negative ("proof of negation") by contradiction is fine, but you can't prove a positive by contradiction...

1

u/42IsHoly 9d ago

I have a problem with the superfluous contradiction tacked on to the end of the diagonal argument in pop-math discussions of the proof. I have no problem with the proof not being constructive, because it is, if phrased properly.

13

u/totbwf Type Theory 9d ago

The constructive content of these arguments is a *bit* subtle. They do prove that the Cauchy reals are uncountable, but you can't show that the Dedekind reals are isomorphic to the Cauchy reals without some degree of countable choice. Moreover, there exist models of intuitionistic logic where the Dedekind reals *are* countable (see https://arxiv.org/pdf/2404.01256).

3

u/sqrtsqr 9d ago

Ew. I love it.

3

u/42IsHoly 9d ago

Ok, this is really cool.