Real Closed Field - Model Theory: Decidability and Quantifier Elimination

Model Theory: Decidability and Quantifier Elimination

The theory of real closed fields was invented by algebraists, but taken up with enthusiasm by logicians. By adding to the ordered field axioms

• an axiom asserting that every positive number has a square root, and
• an axiom scheme asserting that all polynomials of odd degree have at least one root,

one obtains a first-order theory. Tarski (1951) proved that the theory of real closed fields in the first order language of partially ordered rings (consisting of the binary predicate symbols "=" and "≤", the operations of addition, subtraction and multiplication and the constant symbols 0,1) admits elimination of quantifiers. The most important model theoretic consequences hereof: The theory of real closed fields is complete, o-minimal and decidable.

Decidability means that there exists at least one decision procedure, i.e., a well-defined algorithm for determining whether a sentence in the first order language of real closed fields is true. Euclidean geometry (without the ability to measure angles) is also a model of the real field axioms, and thus is also decidable.

The decision procedures are not necessarily practical. The algorithmic complexities of all known decision procedures for real closed fields are very high, so that practical execution times can be prohibitively high except for very simple problems.

The algorithm Tarski proposed for quantifier elimination has NONELEMENTARY complexity, meaning that no tower can bound the execution time of the algorithm if n is the size of the problem. Davenport and Heintz (1988) proved that quantifier elimination is in fact (at least) doubly exponential: there exists a family Φ_n of formulas with n quantifiers, of length O(n) and constant degree such that any quantifier-free formula equivalent to Φ_n must involve polynomials of degree and length, using the Ω asymptotic notation. Ben-Or, Kozen, and Reif (1986) proved that the theory of real closed fields is decidable in exponential space, and therefore in doubly exponential time.

Basu and Roy (1996) proved that there exists a well-behaved algorithm to decide the truth of a formula ∃x₁,…,∃x_k P₁(x₁,…,x_k)⋈0∧…∧P_s(x₁,…,x_k)⋈0 where ⋈ is <, > or =, with complexity in arithmetic operations sk+1dO(k). In fact, the existential theory of the reals can be decided in PSPACE.