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 the extended version is still decidable, 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?

Turing machines, in the classical sense, decide languages of finite strings over finite alphabets. Your logical language has uncountably many constant symbols so you can't even write down all the formulas as strings, let alone ask a Turing machine to decide things about the collection of formulas.

StackExchange Computer Science Q#43217, answer score: 5