of the ordered field of rational numbers is the field of real algebraic numbers. The theorem is named for Emil Artin and Otto Schreier, who proved it in 1926. If (F, P) is an ordered field, and E is a Galois extension of F, then by Zorn's lemma there is a maximal ordered field extension (M, Q) with M a subfield of E containing F and the order on M extending P. This M, together with its ordering Q, is called the relative real closure of (F, P) in E. We call (F, P) real closed relative to E if M is just F. When E is the algebraic closure of F the relative real closure of F in E is actually the real closure of F described earlier. If F is a field (no ordering compatible with the field operations is assumed, nor is it assumed that F is orderable) then F still has a real closure, which may not be a field anymore, but just a real closed ring. For example, the real closure of the field is the ring (the two copies correspond to the two orderings of ). On the other hand, if is considered as an ordered subfield of , its real closure is again the field . Decidability and quantifier elimination The language of real closed fields includes symbols for the operations of addition and multiplication, the constants 0 and 1, and the order relation (as well as equality, if this is not considered a logical symbol). In this language, the (first-order) theory of real closed fields, , consists of the following: the axioms of ordered fields; the axiom asserting that every positive number has a square root; for every odd number , the axiom asserting that all polynomials of degree have at least one root. All of the above axioms can be expressed in first-order logic (i.e. quantification ranges only over elements of the field). Tarski proved () that is complete, meaning that for any -sentence, it can be proven either true or false from the above axioms. Furthermore, is decidable, meaning that there is an algorithm to decide the truth or falsity of any such sentence. The Tarski–Seidenberg theorem extends this result to decidable quantifier elimination. That is, there is an algorithm that, given any -formula, which may contain free variables, produces an equivalent quantifier-free formula in the same free variables, where