> A “useful real” is just a real number that can be precisely described (not just approximated!) by some symbolic notation. Obviously, this definition is loose and depends greatly on your choice of symbols and their definitions.
In fact, the definition is necessarily loose. If you could make it precise then you could carry out Cantor's diagonalisation procedure to produce a precise description of a real which couldn't be precisely described, a contradiction.
You can make it precise if the language in which you define a "useful real" is richer than the language in which individual useful reals must be defined. For instance, model theorists will talk about definable reals in a model of set theory: https://en.wikipedia.org/wiki/Definable_real_number#Definabi...
> A real number a is first-order definable in the language of set theory, without parameters, if there is a formula φ in the language of set theory, with one free variable, such that a is the unique real number such that φ(a) holds (see Kunen 1980, p. 153). This notion cannot be expressed as a formula in the language of set theory.
It seems to me that Cantor's diagonalization fails here because of the very different nature of descriptions vs (for example) decimal notation. Every possible string of digits is a valid, unique number. That does not apply to descriptions.
I'd assume that every number that can be precisely described by some symbolic notation can be described in that notation in multiple ways, and likely in an infinite number of multiple different ways. E.g. the number 2 can be described as 1+1, 1+1+1-1, 1+1+1+1-1-1, ad infinitum.
Furthermore, I'd assume that not every string in that symbolic notation constitutes a valid, precise description of some real.
So Cantor's diagonalization produces some unique description of a number that differs from all of the descriptions - but it's possible and plausible that the description refers to a number that is in the list but has been described differently; and it's possible and plausible that the constructed description does not describe any real whatsoever.
Or am I completely misunderstanding you and you did not intend to apply Cantor's diagonalization to the descriptions?
I don't mean to apply the diagonalisation procedure to the descriptions. That wouldn't work for the reason you mentioned, and also because applying Cantor's diagonalisation to a bunch of finite strings might yield an infinite string.
What I meant was to apply Cantor's diagonalisation to the decimal expansions of the describable numbers. Take all of the describable numbers ordered lexicographically by their lexicographically first description, and then look at their decimal expansions and describe a new number that differs from the nth one in the nth decimal place (with the usual details to make sure you don't end up with a second representation of a number already present).
This gives the decimal expansion of an alegedly indescribable number, because it's different from all the ones on the list. But because I can describe the diagonalisation procedure, this decimal expansion is itself a valid description, and hence we have a contradiction.
> the definition is necessarily loose. If you could make it precise then you could carry out Cantor's diagonalisation procedure to produce a precise description of a real which couldn't be precisely described
Is this true without the Axiom of Choice? Don't you need a choice function to order the numbers before you can diagonalize them?
Finite descriptions are countable. Axiom of Countable Choice is not counterintuitive like Axiom of (Uncountable) Choice.
You can order the set of all definitions, by prepending each definition with its length and then using the ordering (numerical order, alphabetical order).
In this case you can define an order without using Choice. By definition of 'useful number' each useful number has some finite string that describes it. The finite strings can be put into lexicographic order, and then the useful numbers can be ordered according to the position of the lexicographically first string that describes them.
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 but is not definable. This means at the very least we have a mathematical statement saying there exists a number such that some logical predicate is valid (we may not even have a construction in ZFC), which can also be constructed using a Cauchy sequence. This mathematical statement is embedded in ZFC, and since we are humans it must be finite. In fact, you could come up with a binary representation for such a statement using methods from Godel, by mapping each symbol to some binary representation. Therefore, this number can be represented as a sequence of zeros or ones, a contradiction.
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.
I didn't do it that much justice because I was discovering it independently, my arguments can easily be made rigorous, but you'd need a background in pure mathematics to understand it. However, there's a section on Wiki:
In fact, the definition is necessarily loose. If you could make it precise then you could carry out Cantor's diagonalisation procedure to produce a precise description of a real which couldn't be precisely described, a contradiction.