Theory of real closed fields ($\mathrm{RCF}$)

This is the complete first-order theory of real closed fields.

The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.

In the language of ordered rings, the Theory of real closed fields has quantifier elimination. In its pure ring reduct the order is definable by nonzero squares, so model completeness survives, although quantifier elimination does not. Keeping these two language conventions separate is essential when constructing a model companion.

A non-Archimedean real closed field contains a positive element larger than every standard integer. Compactness constructs one by adjoining a constant $c$ and the formulas $c>n$ for all natural numbers $n$.

Model completeness of real closed fields transfers positivity of a rational function from $\mathbb{R}$ to real closed extensions of $\mathbb{R}$. If the function were not a sum of squares, the Artin-Schreier ordering criterion would produce a real closure in which it is negative, giving a contradiction.