3 ms·

Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathemat

by mafribe 11y ago

Rest assured that (contrary to j2kun's misleading claims) if some of the world's top mathematicians and computer scientists propose a new foundation of mathematics, they don't forget real numbers. You need to distinguish between non-computable and non-constructive. The proof that the cardinality of the reals is non-countable is perfectly constructive, see [1] for a discussion of these and related issues. [1] https://en.wikipedia.org/wiki/Cantor%27s_first_uncountability_proof#Constructive_or_non-constructive_nature_of_Cantor.27s_proof_of_the_existence_of_transcendentals https://en.wikipedia.org/wiki/Cantor%27s_first_uncountabilit...

igravious 11y ago
Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded. Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals. Where am I going wrong? NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.
- 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 ago
    Exactly. 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 ago
    Yes, 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 :)
baddox 11y ago
I'm familiar with the diagonal argument, but the version I learned in Discrete Math courses defines the reals as little more than a (potentially infinite) series of digits with a decimal point somewhere, which I thought didn't hold up to much scrutiny. But this stuff is way above my mathematics pay grade. :) I stumbled onto the Wikipedia article "Construction of the real numbers" and I have no clue what is going on. https://en.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.wikipedia.org/wiki/Construction_of_the_real_numbe...

by mafribe 11y ago

igravious 11y ago

Eh? Your very own link says that there is debate within the mathematical community about whether Cantor's uncountability proof is constructive or not. I just realised that in my mind uncountable (not in a one-to-one correspondence with the natural numbers) means non-constructive. For me countability just says that we have a (constructive) method for generating a sequence of what would be all the terms in the sequence (if it were ever to terminate which it doesn't) and no term outside the sequence in a non-repeating fashion that is unbounded. Clearly if some sequence is uncountable it means that one of these criteria fails to hold. Which one? Not the non-repeating stipulation. Not the no term outside the sequence stipulation. It must be the stipulation that every term will be encountered during the generation. So there isn't a (constructive) method for generating uncountable sequences. The reals are uncountable, ergo there is no constructive method for generating the reals. Where am I going wrong? NB: I am not saying that you can't have a method for constructing individual reals like e and pi and so on.

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 ago
  Exactly. 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 ago
  Yes, 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 :)

baddox 11y ago

I'm familiar with the diagonal argument, but the version I learned in Discrete Math courses defines the reals as little more than a (potentially infinite) series of digits with a decimal point somewhere, which I thought didn't hold up to much scrutiny. But this stuff is way above my mathematics pay grade. :) I stumbled onto the Wikipedia article "Construction of the real numbers" and I have no clue what is going on. https://en.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.wikipedia.org/wiki/Construction_of_the_real_numbe...