Formally real field

In mathematics, in particular in field theory and real algebra, a formally real field is a field that can be equipped with a (not necessarily unique) ordering that makes it an ordered field.

Alternative Definitions

The definition given above is not a first-order definition, as it requires quantifiers over sets. 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 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.) This can be expressed in first-order logic by [math]\displaystyle{ \forall x_1 (-1 \ne x_1^2) }[/math], [math]\displaystyle{ \forall x_1 x_2 (-1 \ne x_1^2 + x_2^2) }[/math], etc., one sentence for each number of variables.
• There exists an element of F that 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 that 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, and the non-negative elements are exactly the squares.

References

• Milnor, John; Husemoller, Dale (1973). Symmetric bilinear forms. Springer. ISBN 3-540-06009-X. 
• Rajwade, A. R. (1993). Squares. London Mathematical Society Lecture Note Series. 171. Cambridge University Press. ISBN 0-521-42668-5. 

pl:Ciało (formalnie) rzeczywiste