Artin–Schreier theorem on formally real fields

Remarks

One direction is short: in an ordered field every square is nonnegative, so every sum of squares is nonnegative and cannot equal $-1$. For the converse, let $\Sigma$ be the set of sums of squares of $F$. If $F$ is formally real, then $\Sigma$ is closed under addition and multiplication and does not contain $-1$. By Zorn's lemma, there is a maximal subset $P \supseteq \Sigma$ with these properties, and one shows that $P$ is the set of nonnegative elements of an ordering of $F$. Example: $\Q(\sqrt{2})$ is formally real, and it has two orderings, one with $\sqrt{2} > 0$ and one with $\sqrt{2} < 0$. Example: $\C$ is not formally real, since $-1 = i^2$, and so $\C$ has no field ordering.

Going deeper

For a student

The theorem is the starting point of real algebra and of the theory of real closed fields developed by Artin and Schreier. Its proof shows more: the orderings of a formally real field correspond to the maximal subsets $P$ described above. The same theory shows that every formally real field has an algebraic extension that is real closed. Artin used this theory in his solution of Hilbert's seventeenth problem, which asks whether a nonnegative real polynomial is a sum of squares of rational functions. The Artin–Schreier theorem on fields with algebraic closure of finite degree belongs to the same theory.