Necessity of formal realness

We can define an ordered field axiomatically as a totally ordered field that has two conditions (1) additive monotonicity which is that if $a < b$ then for all $x$ it is the case that $a+x < b+x$ and (2) multiplicative positivity preservation which means that for all $0 < a$ and $0 < b$ then $0 < ab$. We will prove several theorems that describe other properties of ordered fields.

Theorem. the sum of positive elements is positive

Let $a$ and $b$ be two positive elements. By positivity we have that $0 < a$ and $0 < b$. By the fact that $0 < a$ we can add $b$ to both sides to get $b < a+b$. Then connecting that with the previous inequality $0 < b$ we get $0 < b < a+b$ which by transitivity means that $0 < a+b$.

Theorem. the additive inverse of a negative number is positive

Let $a$ be a negative number. By negativity we have that $a < 0$. By additive monotonicity we know that $-a$ is an additive monotone element which can be added to both sides to get $a+(-a) < 0+(-a)$ which equals $0 < (-a)$ which means that the additive inverse $(-a)$ is greater then zero and therefore positive.

Theorem. addition must be torsion-free

In order for a group to be torsion-free it must not have any elements that are of finite order. Suppose that we have a field that has a non-identity additive torsion element, then there are two cases (1) the element is positive in which case the fact that the element can be added to itself to get zero defies additive positivity preservation or (2) the element is negative in which case its additive inverse is a positive torsion element which can be added to itself to get zero which also defies additive positivity preservation. So by contradiction we know that the additive group of the ordered field must be torsion-free.

Previously we touched on the two essentially types of properties of algebraic operations (1) an element being non-periodic and (2) an element being torsion-free. Being torsion-free is the weaker condition. These two properties are related to rather or not an algebraic structure can be ordered. It is actually intuitive that a non torsion-free group cannot be ordered, because it has some element that exhibits unordered cyclical behavior. So we can get a special case of this theorem, which is that any ordered group must be torsion-free.

Corollary. the characteristic of the field is zero

Theorem. the square of any non-zero number is positive.

By the total ordering of the field we can split this up into two cases (1) the element is positive and (2) the element is negative. In the first case that the element is positive we know that its square is positive by positivity preservation which is axiomatic. In the second case that the element is negative, by a previous theorem we know that its additive inverse is a positive number $p$. By the fact that the additive inverse is an involution this means that this number can be expressed as $-p$. Then consider the square as $(-p)^2$. This is equal to $(-1)^2*p^2$. We can cancel out the $(-1)^2$ to get $p^2$. By positivity preservation this again a positive number. This means that the product of any non-zero number with itself is positive.

Theorem. there are no proper zero sums of squares in an ordered field.

By the fact that the square of a non-zero number is positive and that the sum of positive numbers is again a positive number, we know that the sum of the squares of non-zero numbers is positive and therefore not equal to zero. This means that there are no proper zero sums of squares.

Conclusion. in order for a field to be orderable it must be formally real