[gweinberg]

That's what I would think. But since the set of reals is clearly uncountable, it seems to me that the precise membership of the real numbers cannot be unambiguously defined. There must be uncountably many reals that are not the solution of any equation that can be made using a finite number of characters. But if a "real" number cannot be specified, in what sense does the number exist?

[velis_vel]

If you want to take a constructivist viewpoint, it doesn't exist. You can define constructible analysis, where you only work with numbers that you can approximate arbitrarily well using a Turing machine (this is a subset of all numbers that you can define, since you can do tricks with the halting problem). But constructible numbers still don't have decidable equality, since the halting problem reduces to constructible equality: is the number whose 2^-ith place is 1 if and only if the Turing machine M halts on the ith step equal to 0? You can approximate it arbitrarily well by running M for more and more steps, but proving that it's 0 would require proving that M never halts. (You can, however, get decidable ordering if you know a priori two numbers are unequal, simply by approximating them close enough that you can distinguish them.)

Personally, I'm not a constructivist; I think that these undefinable real numbers exist just as well as the ones that we can define. But that's a philosophical argument and I was never any good at those.