Formally real field
|This article needs additional citations for verification. (December 2009)|
The definition given above is not a first-order definition, as it requires quantifiers over sets. However, the following criteria can be coded as first-order sentences in the language of fields, and are equivalent to the above definition.
- −1 is not a sum of squares in F. In other words, the Stufe of F is infinite. (In particular, such a field must have characteristic 0, since in a field of characteristic p the element −1 is a sum of 1's.)
- There exists an element of F which is not a sum of squares in F, and the characteristic of F is not 2.
- If any sum of squares of elements of F equals zero, then each of those elements must be zero.
It is easy to see that these three properties are equivalent. It is also easy to see that a field which admits an ordering must satisfy these three properties.
A proof that if F satisfies these three properties, then F admits an ordering uses the notion of prepositive cones and positive cones. 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.
Real Closed Fields
A formally real field with no formally real proper algebraic extension is a real closed field. 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.
- Rajwade, Theorem 15.1.
- Milnor and Husemoller (1973) p.60
- Rajwade (1993) p.216