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

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.

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.