Extensions of Orderings

In this article we extend the algebraic theory of ordered fields [6], [8] in Mizar. We introduce extensions of orderings: if E is a field extension of F, then an ordering P of F extends to E, if there exists an ordering O of E containing P. We first prove some necessary and su cient conditions for P being extendable to E, in particular that P extends to E if and only if the set QS E:={ ∑ a*b2|a∈P, b∈E } QS\,\,E: = \left\{ {\sum {a*{b^2}|a \in P,\,\,b \in E} } \right\} is a preordering of E – or equivalently if and only if −1 / ∉ QS E. Then we show for non-square a ∈ F that P extends to F(a) F\left( {\sqrt a } \right) if and only if P and finally that every ordering P of F extends to E if the degree of E over F is odd.