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.
In this language, the (first-order) theory of real closed fields,
, consists of all sentences that follow from the following axioms: All of these axioms can be expressed in first-order logic (i.e. quantification ranges only over elements of the field).
is just the set of all first-order sentences that are true about the field of real numbers.
is decidable, meaning that there is an algorithm to determine the truth or falsity of any such sentence.
Since the truth of quantifier-free formulas without free variables can be easily checked, this yields the desired decision procedure.
If R is a real closed field, a formula with n free variables defines a subset of Rn, the set of the points that satisfy the formula.
Given a subset of k variables, the projection from Rn to Rk is the function that maps every n-tuple to the k-tuple of the components corresponding to the subset of variables.
The projection theorem asserts that a projection of a semialgebraic set is a semialgebraic set, and that there is an algorithm that, given a quantifier-free formula defining a semialgebraic set, produces a quantifier-free formula for its projection.
The decidability of a first-order theory of the real numbers depends dramatically on the primitive operations and functions that are considered (here addition and multiplication).
Adding other functions symbols, for example, the sine or the exponential function, can provide undecidable theories; see Richardson's theorem and Decidability of first-order theories of the real numbers.
Furthermore, the completeness and decidability of the first-order theory of the real numbers (using addition and multiplication) contrasts sharply with Gödel's and Turing's results about the incompleteness and undecidability of the first-order theory of the natural numbers (using addition and multiplication).
There is no contradiction, since the statement "x is an integer" cannot be formulated as a first-order formula in the language
Tarski's original algorithm for quantifier elimination has nonelementary computational complexity, meaning that no tower can bound the execution time of the algorithm if n is the size of the input formula.
The cylindrical algebraic decomposition, introduced by George E. Collins, provides a much more practicable algorithm of complexity where n is the total number of variables (free and bound), d is the product of the degrees of the polynomials occurring in the formula, and O(n) is big O notation.
Davenport and Heintz (1988) proved that this worst-case complexity is nearly optimal for quantifier elimination by producing a family Φn of formulas of length O(n), with n quantifiers, and involving polynomials of constant degree, such that any quantifier-free formula equivalent to Φn must involve polynomials of degree
For the decision problem, Ben-Or, Kozen, and Reif (1986) claimed to have proved that the theory of real closed fields is decidable in exponential space, and therefore in double exponential time, but their argument (in the case of more than one variable) is generally held as flawed; see Renegar (1992) for a discussion.
Basu and Roy (1996) provided a well-behaved algorithm to decide the truth of such an existential formula with complexity of sk+1dO(k) arithmetic operations and polynomial space.
A crucially important property of the real numbers is that it is an Archimedean field, meaning it has the Archimedean property that for any real number, there is an integer larger than it in absolute value.
The Archimedean property is related to the concept of cofinality.
In other words, X is an unbounded sequence in F. The cofinality of F is the cardinality of the smallest cofinal set, which is to say, the size of the smallest cardinality giving an unbounded sequence.
We have therefore the following invariants defining the nature of a real closed field F: To this we may add These three cardinal numbers tell us much about the order properties of any real closed field, though it may be difficult to discover what they are, especially if we are not willing to invoke the generalized continuum hypothesis.
There are also particular properties that may or may not hold: The characteristics of real closed fields become much simpler if we are willing to assume the generalized continuum hypothesis.
This unique field Ϝ can be defined by means of an ultrapower, as
, where M is a maximal ideal not leading to a field order-isomorphic to
This is the most commonly used hyperreal number field in nonstandard analysis, and its uniqueness is equivalent to the continuum hypothesis.
It can be seen to be the higher-dimensional analogue of the real numbers; with cardinality
Using those axioms, one can show that the points on a line form a real closed field R, and one can introduce coordinates so that the Euclidean plane is identified with R2 .
Employing the decidability of the theory of real closed fields, Tarski then proved that the elementary theory of Euclidean geometry is complete and decidable.