= Solution
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\geq1$, the sentence
$$
\forall x_1\cdots\forall x_m\ \bigl(1+x_1^2+\cdots+x_m^2\ne0\bigr).
$$
A <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 is
$$
\forall a\,\exists b\,(a=b^2\vee -a=b^2),
$$
and the polynomial axioms say that every monic polynomial of degree $2d+1$ has a root, for each $d\geq0$.
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 by
$$
a>0\quad\Longleftrightarrow\quad a\ne0\text{ and }\exists b\,(b^2=a).
$$
Any <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> prove
$$
\boxed{\mathrm{RCF}\text{ is the model companion of }\mathrm{FRF}.}
$$
The <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.
Back to article page
