You are looking in the wrong place for the key philosophical issue, but didn't land on it.
When we talk about "an infinite sequence of digits", what are we talking about? Are we talking about ACTUALLY having an infinite sequence of digits in front of us? Or are we talking about having a RULE that will in theory produce them?
Platonists believe that they actually exist in a reality beyond human conceptual limits. (Maybe in the mind of God?) Formalists side step the question by making everything an abstract symbol manipulation game. (Though the rules of the game are chosen to result in something matching platonic intuition.) And Constructivists take the rule approach, and not just that, but a rule that we can write down and actually evaluate.
Cantor's diagonalization argument obviously works according to Platonists. Formalists choose their rules to make it work as well. But Constructivists, well, it doesn't work there!
Why not? Well when you get down to it, how do you define a rule and how do you prove that it works? Well, a "rule" can be thought of as just a computer program. And now we have the problem that, thanks to the Halting Problem, it is impossible in general for one computer program to predict what another program will do!
You can, of course, attempt to write Cantor's number down. You can implement the rule that he describes using a theorem prover to filter a list of all programs to just the ones that we can prove are numbers. We can write a perfectly well-defined program that produces Cantor's number. BUT THERE IS NO CONTRADICTION?
Why not?
Because THAT program is one that the theorem prover CAN'T prove works! (In fact the theorem prover will prove what it is doing, and prove that if it always works, then its set of axioms is consistent. And now you're up against Gödel's Incompleteness Theorem!)
The result is that in the two most popular philosophies of math, Cantor's argument works. But in the third, it doesn't, it can't, and the reals are countable. There the complications of diagonalization are simply another illustrations of the challenges of self-reference, and not the assertion that more numbers exist than can be written down!
> But in the third, it doesn't, it can't, and the reals are countable
Isn't that a bit of an overreach? It seems that in Constructivism, Cantor's diagonalization doesn't work as a proof. But that doesn't mean that the reals are countable, just that this proof isn't valid.
Well, you have to be careful about what countable means.
If countable means "put into a one to one correspondence with" then the reals are not countable because there are pairs of reals that can be proven to be real whose equality or inequality can't be proven. So in such cases you can overcount, or undercount, but you can never exactly pick each real only once.
But the set of possible constructions can be enumerated. We may not know which actually are real numbers, and which pairs are equal. But we can list all of the possibilities. So there is a countable list of things that contains them all..multiple times..along with other stuff.
When we talk about "an infinite sequence of digits", what are we talking about? Are we talking about ACTUALLY having an infinite sequence of digits in front of us? Or are we talking about having a RULE that will in theory produce them?
Platonists believe that they actually exist in a reality beyond human conceptual limits. (Maybe in the mind of God?) Formalists side step the question by making everything an abstract symbol manipulation game. (Though the rules of the game are chosen to result in something matching platonic intuition.) And Constructivists take the rule approach, and not just that, but a rule that we can write down and actually evaluate.
Cantor's diagonalization argument obviously works according to Platonists. Formalists choose their rules to make it work as well. But Constructivists, well, it doesn't work there!
Why not? Well when you get down to it, how do you define a rule and how do you prove that it works? Well, a "rule" can be thought of as just a computer program. And now we have the problem that, thanks to the Halting Problem, it is impossible in general for one computer program to predict what another program will do!
You can, of course, attempt to write Cantor's number down. You can implement the rule that he describes using a theorem prover to filter a list of all programs to just the ones that we can prove are numbers. We can write a perfectly well-defined program that produces Cantor's number. BUT THERE IS NO CONTRADICTION?
Why not?
Because THAT program is one that the theorem prover CAN'T prove works! (In fact the theorem prover will prove what it is doing, and prove that if it always works, then its set of axioms is consistent. And now you're up against Gödel's Incompleteness Theorem!)
The result is that in the two most popular philosophies of math, Cantor's argument works. But in the third, it doesn't, it can't, and the reals are countable. There the complications of diagonalization are simply another illustrations of the challenges of self-reference, and not the assertion that more numbers exist than can be written down!