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 ∃x1,…,∃xk P1(x1,…,xk)⋈0∧…∧Ps(x1,…,xk)⋈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.
Read more about this topic: Real Closed Field
Famous quotes containing the words model and/or elimination:
“She represents the unavowed aspiration of the male human being, his potential infidelity—and infidelity of a very special kind, which would lead him to the opposite of his wife, to the “woman of wax” whom he could model at will, make and unmake in any way he wished, even unto death.”
—Marguerite Duras (b. 1914)
“To reduce the imagination to a state of slavery—even though it would mean the elimination of what is commonly called happiness—is to betray all sense of absolute justice within oneself. Imagination alone offers me some intimation of what can be.”
—André Breton (1896–1966)