Formally real field

In mathematics, a formally real field in field theory is a field that shares certain algebraic properties with the real number field. A formally real field "F" may be characterized in any of the following equivalent ways:

* −1 is not a sum of squares in "F". (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, each of those elements must equal zero.
* "F" admits an ordering which makes it an ordered field. (There may be more than one way to do this, so this condition says "F" is orderable in some manner to make it an ordered field.)

The equivalence of the first three properties is easy, and the fourth property easily implies the first three, but it is not easy to show either of the first three properties implies the fourth (that is, it is not evident how the assumption that a sum of squares being 0 forces each square to be 0 actually implies "F" has some ordering as a field).

A formally real field with no formally real algebraic extension is a real closed field.