[proofplan]
We prove quantifier elimination from the semialgebraic [projection theorem](/theorems/1985). First we reduce to formulas with one existential quantifier in front of a quantifier-free formula. A quantifier-free ordered-ring formula defines a semialgebraic subset of affine space over any real closed field. The [Tarski-Seidenberg projection theorem](/theorems/4316) says that the coordinate projection of such a set is again semialgebraic, hence definable by a quantifier-free ordered-ring formula. Eliminating existential quantifiers one at a time then removes all quantifiers.
[/proofplan]
[step:Reduce the proof to one existential quantifier]
Let $R$ be a real closed field. It is enough to eliminate formulas of the form
\begin{align*}
\exists y\,\theta(x_1,\dots,x_n,y),
\end{align*}
where $\theta(x_1,\dots,x_n,y)$ is quantifier-free. Indeed, every first-order formula is obtained from atomic formulas by finitely many Boolean connectives and quantifiers. Boolean combinations of quantifier-free formulas are quantifier-free, and a universal quantifier can be rewritten as
\begin{align*}
\forall y\,\alpha
\quad\Longleftrightarrow\quad
\neg\exists y\,\neg\alpha.
\end{align*}
Thus a finite induction on the number of quantifiers proves full quantifier elimination once the one-existential case is known.
[guided]
We first isolate the only operation that needs work. Let $R$ be a real closed field, and suppose that $\theta(x_1,\dots,x_n,y)$ is quantifier-free. The target is to replace
\begin{align*}
\exists y\,\theta(x_1,\dots,x_n,y)
\end{align*}
by a quantifier-free formula in the variables $x_1,\dots,x_n$.
This suffices for arbitrary formulas because quantifiers are removed from the inside out. Boolean connectives do not introduce new quantifiers, and the identity
\begin{align*}
\forall y\,\alpha
\quad\Longleftrightarrow\quad
\neg\exists y\,\neg\alpha
\end{align*}
turns universal quantifiers into existential quantifiers plus Boolean operations. Since a formula has only finitely many quantifiers, repeatedly applying the one-existential elimination step eventually gives a quantifier-free formula.
[/guided]
[/step]
[step:Translate a quantifier-free formula into a semialgebraic set]
Fix a quantifier-free $L_{\mathrm{or}}$-formula $\theta(x_1,\dots,x_n,y)$. Every ordered-ring term in the variables $x_1,\dots,x_n,y$ is represented by a polynomial with integer coefficients. Therefore each atomic formula is equivalent over ordered rings to one of the forms
\begin{align*}
p(x_1,\dots,x_n,y)=0,
\qquad
p(x_1,\dots,x_n,y)>0,
\qquad
p(x_1,\dots,x_n,y)<0,
\end{align*}
with $p\in\mathbb Z[x_1,\dots,x_n,y]$. Hence, for every real closed field $R$, the solution set
\begin{align*}
S_R
:=
\{(a,b)\in R^n\times R: R\models \theta(a,b)\}
\end{align*}
is a finite Boolean combination of polynomial equalities and strict inequalities. Thus $S_R$ is a semialgebraic subset of $R^{n+1}$.
[guided]
Now fix the quantifier-free formula $\theta(x_1,\dots,x_n,y)$. In the language
\begin{align*}
L_{\mathrm{or}}=\{0,1,+,-,\cdot,<\},
\end{align*}
terms are polynomial expressions. Thus every atomic formula can be rewritten, over ordered rings, as a polynomial equation or a strict polynomial inequality:
\begin{align*}
p(x_1,\dots,x_n,y)=0,
\qquad
p(x_1,\dots,x_n,y)>0,
\qquad
p(x_1,\dots,x_n,y)<0,
\end{align*}
where $p\in\mathbb Z[x_1,\dots,x_n,y]$.
Because $\theta$ is quantifier-free, it is a finite Boolean combination of such atomic sign conditions. For a real closed field $R$, define
\begin{align*}
S_R
:=
\{(a,b)\in R^n\times R: R\models \theta(a,b)\}.
\end{align*}
The preceding description shows that $S_R$ is a finite Boolean combination of polynomial equalities and strict inequalities in $R^{n+1}$. This is exactly the definition of a semialgebraic subset of $R^{n+1}$.
[/guided]
[/step]
[step:Project the semialgebraic set and convert back to a formula]
Let
\begin{align*}
\pi:R^{n+1}&\to R^n\\
(a,b)&\mapsto a
\end{align*}
be the coordinate projection. We use the coefficient-uniform form of the Tarski-Seidenberg projection theorem: from any finite Boolean combination of sign conditions on polynomials in
\begin{align*}
\mathbb Z[x_1,\dots,x_n,y],
\end{align*}
there is a finite Boolean combination of sign conditions on polynomials in
\begin{align*}
\mathbb Z[x_1,\dots,x_n]
\end{align*}
which defines its coordinate projection over every real closed field. Applied to the Boolean combination defining $S_R$, this gives one quantifier-free $L_{\mathrm{or}}$-formula $\psi(x_1,\dots,x_n)$, depending only on $\theta$ and not on $R$, such that for every real closed field $R$ and every $a\in R^n$,
\begin{align*}
a\in \pi(S_R)
\quad\Longleftrightarrow\quad
R\models \psi(a).
\end{align*}
By definition of $\pi(S_R)$,
\begin{align*}
a\in \pi(S_R)
\quad\Longleftrightarrow\quad
\text{there exists } b\in R \text{ such that } R\models \theta(a,b).
\end{align*}
Therefore
\begin{align*}
R\models \exists y\,\theta(a,y)
\quad\Longleftrightarrow\quad
R\models \psi(a)
\end{align*}
for every real closed field $R$ and every $a\in R^n$.
[guided]
We now remove the existential quantifier geometrically. Let the coordinate projection be
\begin{align*}
\pi:R^{n+1}&\to R^n\\
(a,b)&\mapsto a.
\end{align*}
The previous step proved that $S_R\subseteq R^{n+1}$ is semialgebraic. The [Tarski-Seidenberg Projection Theorem](/theorems/???) applies because $R$ is real closed, $S_R$ is semialgebraic over $R$, and $\pi$ is the standard coordinate projection. It gives that $\pi(S_R)$ is semialgebraic in $R^n$.
We use the theorem in its uniform algebraic form. The input Boolean combination uses only the integer-coefficient polynomials occurring in $\theta$. The output is therefore a single Boolean combination of sign conditions on integer-coefficient polynomials in $x_1,\dots,x_n$. Equivalently, there is one quantifier-free formula $\psi(x_1,\dots,x_n)$ in $L_{\mathrm{or}}$, independent of the real closed field $R$, such that
\begin{align*}
a\in \pi(S_R)
\quad\Longleftrightarrow\quad
R\models \psi(a)
\end{align*}
for every real closed field $R$ and every $a\in R^n$.
Finally, by the definition of projection,
\begin{align*}
a\in \pi(S_R)
\quad\Longleftrightarrow\quad
\text{there exists } b\in R \text{ with } (a,b)\in S_R
\quad\Longleftrightarrow\quad
R\models \exists y\,\theta(a,y).
\end{align*}
Combining the equivalences gives
\begin{align*}
R\models \exists y\,\theta(a,y)
\quad\Longleftrightarrow\quad
R\models \psi(a).
\end{align*}
Thus the one-existential formula is equivalent over real closed fields to a quantifier-free formula.
[/guided]
[/step]
[step:Iterate the elimination to prove quantifier elimination]
Apply the previous step repeatedly to the innermost existential quantifier of a formula, using
\begin{align*}
\forall y\,\alpha
\quad\Longleftrightarrow\quad
\neg\exists y\,\neg\alpha
\end{align*}
for universal quantifiers. Each iteration strictly decreases the number of quantifiers and preserves equivalence in every real closed field. Therefore, for the original formula $\varphi(x_1,\dots,x_n)$, there is a quantifier-free $L_{\mathrm{or}}$-formula $\psi(x_1,\dots,x_n)$ such that
\begin{align*}
\mathrm{RCF} \models \forall x_1\cdots\forall x_n\,
\bigl(\varphi(x_1,\dots,x_n)\leftrightarrow \psi(x_1,\dots,x_n)\bigr).
\end{align*}
This is quantifier elimination for $\mathrm{RCF}$.
[guided]
The preceding step eliminates one existential quantifier whose matrix is quantifier-free. To handle an arbitrary formula $\varphi(x_1,\dots,x_n)$, first rewrite universal quantifiers by
\begin{align*}
\forall y\,\alpha
\quad\Longleftrightarrow\quad
\neg\exists y\,\neg\alpha.
\end{align*}
Then choose an innermost existential quantifier. Its matrix is quantifier-free after the inner quantifiers have already been removed, so the projection argument replaces that subformula by a quantifier-free formula with the same free variables.
Repeating this finite process removes one quantifier at each step. Since equivalence is preserved in every real closed field at each replacement, the final quantifier-free formula $\psi(x_1,\dots,x_n)$ satisfies
\begin{align*}
\mathrm{RCF} \models \forall x_1\cdots\forall x_n\,
\bigl(\varphi(x_1,\dots,x_n)\leftrightarrow \psi(x_1,\dots,x_n)\bigr).
\end{align*}
This proves that $\mathrm{RCF}$ eliminates quantifiers in the ordered-ring language.
[/guided]
[/step]
