3 ms·
Even though there isn't a constructive method of generating uncountable sequences, that doesn't mean that this also assumed from within the logic. In convention
by jules 11y ago
Even though there isn't a constructive method of generating uncountable sequences, that doesn't mean that this also assumed from within the logic. In conventional mathematics you can also only write down countably many sequences, but the space of all sequences is still uncountable. We don't assume that the set of all sequences is the set of sequences which we can actually define. Similarly in constructive mathematics we don't say that ALL sequences are generated by some computer program, just that YOU are only allowed to generate sequences in that way.
So this doesn't contradict in any way that Cantor's proof is constructive (which contrary to that wikipedia article, it most definitely is).
- YorkshireSeason 11y agoExactly. Here is an implementation of Cantor's diagonal method in Agda which is entirely constructive: http://www.playingwithpointers.com/agda-cantor.html http://www.playingwithpointers.com/agda-cantor.html
- igravious 11y agoYes, of course. I was coming dangerously close to conflating the fact of a sequence being uncountable with the proof that the sequence is uncountable being constructive. In other words, having no constructive method for generating the reals is not at all the same thing, of course, as having a proof that the reals are uncountable. In fact having a constructive proof that the reals are uncountable indicates to us that there is no constructive method for generating them! Oof. You have to so careful with this stuff :)