Extensions of Orderings

Abstract

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 sufficient conditions for P being extendable to E, in particular that P extends to E if and only if the set QS E := {∑a ∗ b²| a ∈ P, b ∈ E} 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) 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.