How to show that $\mathbb{R}$ in the language of rings does not admit quantifier elimination? I am studying for an exam in an introductory mathematical logic course. Suppose we are working in the language of rings $\mathcal{L}=(+,-,\cdot,0,1)$. Then $\mathbb{R}$ does not admit quantifier elimination.
First of all I am a bit unsure of what it means for a structure to admit quantifier elimination, but I assume that $\mathbb{R}$ is shorthand for $\operatorname{Th}(\mathbb{R})=\{\phi \text{ an } \mathcal{L}\text{-sentence}\mid \mathbb{R}\models \phi\}$, since in this case it would make sense (quantifier elimination is defined for theories). Please correct me if this is a false assumption.
So now I want to show that $\mathbb{R}$ does not admit quantifier elimination. It seems difficult to choose a specific formula which has no equivalent quantifier-free formula and then showing this is the case. I do however have the following theorem at my disposal:

Let $T$ be an $\mathcal{L}$-theory, $n\geq 1$ a natural number and $\phi(x_1,\ldots,x_n)$ an $\mathcal{L}$-formula. Then the following are equivalent:

*

*There is a quantifier-free $\mathcal{L}$ formula $\psi(x_1,\ldots,x_n)$ such that $\phi$ and $\psi$ are equivalent in $T$.

*Let $\mathcal{M},\mathcal{N}$ be models of $T$ and let $\mathcal{A}$ be a common substructure. Then for any $\overline{a}\in A^n$ one has $\mathcal{M}\models \phi[\overline a]\iff \mathcal{N}\models \phi[\overline a]$.


If we use this, it suffices to find some elementary equivalent sub- or superstructure in which there is a non-true formula which becomes true or vice versa.
For example, one can take $\mathbb{R}_\text{alg}= \{r\in\mathbb{R}\mid \exists 0\neq p(X)\in \mathbb{Q}[X] \text{ such that } p(r)=0\}$. I tried looking at the formula $\exists x x^2+y=z$ but I believe this to be equivalent in both models.
So can anyone help me find a formula which is not equivalent in both models (or in other cases where we do not choose $\mathbb{R}_\text{alg}$). Or is there perhaps a different method which is better suited for this problem? I would prefer a method which is applicable in similar situations as I believe the one I describe is, but any proof is welcome.
 A: Your idea of using a formula defining $\leq$ is a good one, but it will be easier to work with a similar formula that has only one free variable; I suggest $\exists x\,(x^2=y)$.  I also think it's easier (at least in this case) to ignore the model-theoretic criterion and prove directly that $\exists x\,(x^2=y)$ isn't equivalent, in $\mathbb R$, to any quantifier-free formula with only the variable $y$. The key ingredient of that proof will be that (1) any such quantifier-free formula is just a propositional combination of polynomial equations about $y$ (with integer coefficients, but that won't be needed), (2)  polynomial equation about $y$ is either satisfied by all values of $y$ or by only finitely many (here's where it's pleasant to have just one variable), and (3) therefore a quantifier-free, one-variable formula defines a finite or cofinite subset of $\mathbb R$.
A: I agree with Andreas Blass that the argument suggested in his answer is the most straightforward way to see that the theory of the real field does not have QE. But here's a way to see this using the criterion for QE which you quoted in your question.
First of all, the precise strategy you tried cannot work. The theory $\text{RCF}$ of the real field is model complete, which means that if $M\subseteq N$ are both models of $\text{RCF}$, then $M$ is an elementary substructure of $N$. So you cannot "change the truth value" of a formula by moving down to a smaller model or up to a larger model. The syntactic consequence of this is that every formula is equivalent to both an existential and a universal formula.
But we can still use the criterion for QE to show that the formula $\varphi(x)$: $\exists y\, (y^2 = x)$ is not equivalent to a quantifier-free formula. It suffices to find $M\models \text{RCF}$ and $N\models \text{RCF}$ with substructures (not themselves models of $\text{RCF}$) $A\subseteq M$ and $B\subseteq N$ and an isomorphism $f\colon A\cong B$ such that $M\models \varphi(a)$ and $N\not\models \varphi(f(a))$ for some $a\in A$.
Take $M = N = \mathbb{R}$ and $A = B = \mathbb{Q}[\sqrt{2}]$. Now $\mathbb{Q}[\sqrt{2}]$ has an automorphism $f$ mapping $\sqrt{2}\mapsto-\sqrt{2}$. And we have $\mathbb{R}\models \varphi(\sqrt{2})$ but $\mathbb{R}\not\models \varphi(f(\sqrt{2}))$.

One can boil this down to a very concrete argument by repeating the proof of (the easy direction of) the criterion. Suppose for contradiction that $\varphi(x):\exists y\, (y^2 = x)$ is equivalent in $\mathrm{RCF}$ to a quantifier-free formula $\psi(x)$. Since $\sqrt{2}$ is a square in $\mathbb{R}$, $\mathbb{R}\models \varphi(\sqrt{2})$. Since  $\mathbb{R}\models \mathrm{RCF}$, $\mathbb{R}\models \psi(\sqrt{2})$. Since $\psi$ is quantifier-free and $\sqrt{2}\in \mathbb{Q}[\sqrt{2}]$, $\mathbb{Q}[\sqrt{2}]\models \psi(\sqrt{2})$. Since we can map $\sqrt{2}$ to $-\sqrt{2}$ by an automorphism of $\mathbb{Q}[\sqrt{2}]$, $\mathbb{Q}[\sqrt{2}]\models \psi(-\sqrt{2})$. Since $\psi$ is quantifier-free, $\mathbb{R}\models \psi(-\sqrt{2})$. Since $\mathbb{R}\models \mathrm{RCF}$, $\mathbb{R}\models \varphi(-\sqrt{2})$. But this is a contradiction, since $-\sqrt{2}$ is not a square in $\mathbb{R}$.
