Formally real field

This article defines a field property: a property that can be evaluated to true/false for any field.
View a complete list of field properties|View a complete list of field extension properties

Definition

Algebraic definition

A formally real field is a field in which $-1$ is not a sum of squares.

Definition in terms of total ordering

A formally real field is a field for which there exists a total ordering $\leq$ under which the field becomes an ordered field. In other words, $\leq$ satisfies the following conditions:

• $a\leq b$ and $c\leq d$ implies $a+c\leq b+d$.
• $0\leq 1$.
• $a\leq b$ implies $-b\leq -a$.
• $0\leq a$ and $b\leq c$ implies $ab\leq ac$.

Relation with other properties

Stronger properties

• Real-closed field
• Archimedean field
• Euclidean field

Weaker properties

• Field of characteristic zero: For proof of the implication, refer Formally real implies characteristic zero and for proof of its strictness (i.e. the reverse implication being false) refer Characteristic zero not implies formally real.

Metaproperties

Subfield-closedness

This field property is closed under taking subfields. In other words, any subfield of a field with this property also has this property.
View other subfield-closed field properties

Any subfield of a formally real field is also formally real.

Finite-extension-closedness

This field property is closed under taking finite extensions of odd degree. In other words, any finite extension of odd degree of a field having this property also has this property.

Any finite extension of odd degree of a formally real field is also formally real. Further information: Formally real is odd-extension-closed

It is possible to have a field $K$ with subfields $K_{1}$ and $K_{2}$ such that both $K_{1}$ and $K_{2}$ are formally real, but the subfield they generate is not formally real. Further information: Formally real is not composite-closed