Formally real field ($-1\ne {\sum }_{j=1}^m{a}_j^2$)

A field is formally real when $-1$ is not a finite sum of squares. The Artin-Schreier ordering criterion says this is equivalent to the existence of an ordering compatible with the field operations. Such a field has characteristic zero and embeds into a real closed field.

A field can be ordered compatibly with addition and multiplication if and only if it is a formally real field. This ordering criterion concerns real algebra, and is different from Artin–Schreier theory of cyclic extensions in positive characteristic.

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.

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.

Every ordered field has an ordered algebraic real closure. Combined with the Artin-Schreier ordering criterion, every formally real field embeds into a real closed field. This is one embedding direction in the model companion relation between their theories.