Quantifier elimination for real closed fields

Remarks

The theorem is due to Tarski. It suffices to eliminate one existential quantifier in front of a conjunction of polynomial equations and inequalities in one variable $x$. Such a conjunction has a solution exactly when certain sign conditions on the coefficients hold. These conditions can be computed, for instance with Sturm sequences and the intermediate value property of polynomials over a real closed field.

Example: for real closed fields, $$\exists x \, (x^2 + b x + c = 0) \quad \leftrightarrow \quad b^2 - 4c > 0 \ \lor \ b^2 - 4c = 0.$$

Consequences: $\mathrm{RCF}$ is complete, so every real closed field satisfies the same first-order sentences as $\R$; and $\mathrm{RCF}$ is decidable. Geometrically, the projection of a semialgebraic set is semialgebraic, which is the Tarski–Seidenberg theorem.

The symbol $<$ is necessary. In the language of rings alone, the set $\set{x \in \R : \exists y \, (x = y^2)} = [0, \infty)$ is definable, but every quantifier-free definable subset of $\R$ in that language is finite or cofinite.

Going deeper

For a student

Quantifier elimination is the model-theoretic core of real algebraic geometry. It shows that the sets definable in $\R$ with $+$, $\cdot$ and $<$ are exactly the semialgebraic sets, and that projections and images under polynomial maps stay in this class. It gives the completeness of the theory of real closed fields, which transfers results from $\R$ to every real closed field. This transfer gives a short modern proof of Artin's solution of Hilbert's seventeenth problem. It also shows that the theory of $\R$ is o-minimal: every definable subset of the line is a finite union of points and intervals. The analogous result for algebraically closed fields uses only the language of rings.