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.
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] [2]
\forallx1(-1\ne
| 2) | |
| x | |
| 1 |
\forallx1x2(-1\ne
| 2 | |
| x | |
| 1 |
+
| 2) | |
| x | |
| 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.
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 . One uses this positive cone to define an ordering: if and only if 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.
. John . Milnor . John Milnor . Dale . Husemoller . Dale Husemoller . Symmetric bilinear forms . Springer . 1973 . 3-540-06009-X .