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.
> 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.
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?
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.
Is this true without the Axiom of Choice? Don't you need a choice function to order the numbers before you can diagonalize them?
You can order the set of all definitions, by prepending each definition with its length and then using the ordering (numerical order, alphabetical order).
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.
QED
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.