Formally real field

However, the following criteria can be coded as (infinitely many) first-order sentences in the language of fields and are equivalent to the above definition.

A formally real field F is a field that also satisfies one of the following equivalent properties:[1][2] It is easy to see that these three properties are equivalent.

It is also easy to see that a field that admits an ordering must satisfy these three properties.

Suppose −1 is not a sum of squares; then a Zorn's Lemma argument shows that the prepositive cone of sums of squares can be extended to a positive cone P ⊆ F. One uses this positive cone to define an ordering: a ≤ b if and only if b − a belongs to P. A formally real field with no formally real proper algebraic extension is a real closed field.

[3] If K is formally real and Ω is an algebraically closed field containing K, then there is a real closed subfield of Ω containing K. A real closed field can be ordered in a unique way,[3] and the non-negative elements are exactly the squares.