Hacker News Reader

Comment by ogogmad | Hacker News Reader

Proofs that derive a contradiction are perfectly acceptable in constructive mathematics. Indeed, the real numbers are uncountable in constructive mathematics. What is not allowed is elimination of double negatives, which is not present in the above proof.

View on HN

I'm not sure that real numbers are uncountable in constructive mathematics as they are not computable.

See Andrej Bauer's proof that they are indeed uncountable: https://mathoverflow.net/questions/30643/are-real-numbers-co...

I'm still unconvinced.

Is there a specific issue you have with this proof? With respect, I think you may be conflating a constructive proof of the uncountability of the reals with a proof that the set of all computable reals is countable. These are two different claims.

A statement about the reals which is provable under constructive mathematics does not reduce to a statement about the computable reals and vice versa. A set can be constructively definable without all of its elements being constructively enumerable.

Given any explicit sequence of real numbers, it's always possible to generate a number not in that sequence. In fact, this can be done algorithmically using essentially Cantor's method.

A simple diagonalization argument is perfectly constructive.

Yes, and to clarify what I predict might be a point of contention about the necessity of "contradiction" in Cantor's argument, some of the comments in this thread might be helpful: https://reddit.com/r/math/comments/70xeon/why_is_cantors_dia...

Reply on news.ycombinator.com