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.
Best Answer
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$.