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.

A real closure of an ordered field $K$ is a real closed algebraic extension whose order extends the chosen order of $K$. Existence is the real closure theorem; uniqueness holds up to ordered field isomorphism over $K$. A different ordering of a formally real field can produce a different ordered real closure.

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.