3 ms·
Proofs that derive a contradiction are perfectly acceptable in constructive mathematics. Indeed, the real numbers are uncountable in constructive mathematics. W
by ogogmad 6y ago
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.
- adamnemecek 6y agoI'm not sure that real numbers are uncountable in constructive mathematics as they are not computable.
- ogogmad 6y agoSee Andrej Bauer's proof that they are indeed uncountable: https://mathoverflow.net/questions/30643/are-real-numbers-countable-in-constructive-mathematics https://mathoverflow.net/questions/30643/are-real-numbers-co...
- adamnemecek 6y agoI'm still unconvinced.
- fractionalhare 6y agoIs 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.
- ogogmad 6y agoGiven 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.
- millimeterman 6y agoA simple diagonalization argument is perfectly constructive.
- fractionalhare 6y agoYes, 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_diagonalization_argument_taken_as/ https://reddit.com/r/math/comments/70xeon/why_is_cantors_dia...