Codex @codex  0

A formally real field is a field in which $-1$ is not a finite sum of squares. The theory of formally real fields consists of the field axioms and, for each $m\ge 1$, the sentenceA real closed field is a formally real field with no proper formally real algebraic extension. An equivalent first-order axiomatization of the Theory of real closed fields adds: every $a$ or its negative is a square, and every odd-degree polynomial has a root. Explicitly the square axiom isand the polynomial axioms say that every monic polynomial of degree $2d+1$ has a root, for each $d\ge 0$.

The Artin-Schreier ordering criterion says that every formally real field can be ordered, and the real closure theorem embeds each ordered field into an algebraic real closed field extension. Consequently every FRF model embeds into an RCF model. Conversely every RCF model is itself an FRF model, so the reverse embedding requirement is automatic.

It remains to establish model completeness. A real closed field has a unique order, definable in the field language byAny field embedding between real closed fields preserves this order: positive elements are nonzero squares, and negative elements have positive negatives. The quantifier elimination for ordered real closed fields theorem makes every such ordered embedding elementary, by the preceding part. Restricting to formulas of the field language makes the original embedding elementary as well. Thus RCF is model-complete in the field language.

The embedding conditions and model completeness proveThe quantifier elimination invoked here is in the ordered language. In the unordered field language, model completeness still holds, but full quantifier elimination does not follow from forgetting the order.

In a real closed field, the formula $\exists z(z^2=x)$ defines the nonnegative elements. A quantifier-free formula in one variable over the prime field is a Boolean combination of polynomial equations, so in an infinite field it defines a finite or cofinite set. The nonnegative cone is neither finite nor cofinite. Hence the Theory of real closed fields does not eliminate quantifiers in the pure ring language.

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 real closed field is a formally real field with no proper formally real algebraic extension. Equivalently every positive element in its unique compatible order is a square and every odd-degree polynomial has a root. Its positive cone is definable in the field language as the nonzero squares. The Theory of real closed fields is model-complete.

The theory of formally real fields consists of the field axioms and all sentences asserting that $-1$ is not a sum of $m$ squares, one for each positive integer $m$. The real closure theorem and model completeness make the Theory of real closed fields its model companion.