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).
Collins, G. E. "Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition." In Automata Theory
and Formal Languages: 2nd GI Conference, Kaiserslautern, May 20-23, 1975 (Ed.
H. Brakhage). Berlin, Germany: Springer-Verlag, pp. 134-183, 1975. https://doi.org/10.1007/3-540-07407-4_17.Davenport,
J. and Heintz, J. "Real Quantifier Elimination Is Doubly Exponential."
J. Symb. Comput.5, 29-35, 1988.Marker, D. "Model
Theory and Exponentiation." Not. Amer. Math. Soc.43, 753-759,
1996.Strzebonski, A. "Solving Algebraic Inequalities." Mathematica
J.7, 525-541, 2000.Tarski, A. "Sur les ensembles définissables
de nombres réels." Fund. Math.17, 210-239, 1931.Tarski,
A. A Decision Method for Elementary Algebra and Geometry. Manuscript. Santa
Monica, CA: RAND Corp., 1948. Republished as A Decision Method for Elementary
Algebra and Geometry, 2nd ed. Berkeley, CA: University of California Press, 1951.
,
, 
, 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.
