Extended version of the theory of reals and its decidability It is well-known due to Tarski that the theory of reals $(\mathbb{R},+,\cdot,<,=)$ is decidable. I was asking my self whether one would lose the decidability by adding all real constants. More formally, is the theory $(\mathbb{R},\{\underline{r} \mid r \in \mathbb{R}\} +,\cdot,<,=)$ evaluated in the standard model of the reals decidable? Here, the symbol $\underline{r}$ is such that its interpretation in the standard model is exactly the real $r$.
I guess that this is the case, essentially because two reals are different if and only if there exists a rational number between them. Rationals, on the other hand, can be expressed in the usual Tarski fragment. 
Can anyone help?
 A: There's the fundamental problem here that you have now defined a logical language with uncountably many symbols. This means that you also have uncountably many different formulas, which means that you have no way of encoding all formulas uniquely in a way that can be input to a Turing machine.
Therefore it doesn't really make sense to ask whether the theory is decidable -- or at least not without extending the meaning of "decidable" such that it can handle uncountable sets of inputs. And if you do that, it is doubtful how much your resulting notion of "decidable" will have to do with the usual one.
For example, your language has a symbol that corresponds to Chaitin's constant. It will take some extremely careful design to define a class of machines that can manipulate this symbol in a way that feels meaningful without having as a side effect that the halting problem suddenly becomes "decidable".
A: By Theorem 1.1 on page 260 of the book, which is about 1/8 of the way

through the pdf, the extended "version of the theory of reals" is decidable.
