Tarski's Theorem
Tarski's theorem says that the first-order theory of reals with 
, 
, 
, and 
allows quantifier
elimination. Algorithmic quantifier elimination implies decidability
assuming that the truth values of sentences involving only constants can be computed.
However, the converse is not true. For example, the first-order theory of reals with
, 
, and 
is decidable,
but does not allow quantifier elimination.
Tarski's theorem means that the solution set of a quantified system of real algebraic equations and inequations is a semialgebraic set (Tarski 1951, Strzebonski 2000).
Although Tarski proved that quantifier elimination was possible, his method was totally impractical (Davenport and Heintz 1988). A much more efficient procedure for implementing quantifier elimination is called cylindrical algebraic decomposition. It was developed by Collins (1975) and is implemented as CylindricalDecomposition[ineqs, vars].
Contact the MathWorld Team
5*aleph0^aleph0