Earlier quoted context omitted.
Another argument that's not completely non-constructive. The real numbers have to be constructed. Typically, a number is represented by a Cauchy sequence or a Dedekind cut. To determine if a real number is representable symbolically, we simply need a finite sequence of symbols which stands for this Cauchy sequence, lets say. Theroem: The real numbers and definable numbers are the same set. Assume a real number exists…
I don't understand that argument. But in any case, Cantor's argument is very constructive. It literally gives you the decimal expansion of the new number not in your set.
https://en.wikipedia.org/wiki/Definable_real_number#Definabi...
They start with a stronger definition of a definable number, so they find that they do exist.
I think given the argument above there must be a hole in my own argument, I'd have to go beyond ZFC.