nLab Tarski-Seidenberg theorem






The image of a semialgebraic set in R n+1R^{n+1} under the projection map

π:R n+1R n:(x 1,,x n+1)(x 1,,x n) \pi \colon R^{n+1} \to R^n: (x_1, \ldots, x_{n+1}) \mapsto (x_1, \ldots, x_n)

is also a semi-algebraic set.


This powerful theorem is usually understood in the context of formal logic and model theory, where one considers subsets of Euclidean space n\mathbb{R}^n that are definable by first-order logical formulas in the language of ordered rings. It says that the definable subsets are precisely semi-algebraic sets, i.e., sets defined by taking Boolean combinations of sets of the form

{(x 1,,x n) n:p(x 1,,x n)0}\{(x_1, \ldots, x_n) \in \mathbb{R}^n: p(x_1, \ldots, x_n) \geq 0\}

where pp is a polynomial.

In logic, the result is understood as connected to a quantifier elimination result. By definition, semi-algebraic sets XX are definable by formulas PP without any quantifiers. Taking an image under a projection amounts to applying an existential quantifier:

π(X)=π({(x 1,,x n+1) n+1:P(x 1,,x n,x n+1)}={(x 1,,x n) n: x n+1P(x 1,,x n,x n+1)}\pi(X) = \pi(\{(x_1, \ldots, x_{n+1}) \in \mathbb{R}^{n+1}: P(x_1, \ldots, x_n, x_{n+1})\} = \{(x_1, \ldots, x_n) \in \mathbb{R}^n: \exists_{x_{n+1}} P(x_1, \ldots, x_n, x_{n+1})\}

and Tarski-Seidenberg allows us to replace x n+1P\exists_{x_{n+1}} P by some quantifier-free formula. By induction, it follows that any quantified formula may be replaced by a quantifier-free one.

There is a host of consequences of this result, including the fact that the theory Th()Th(\mathbb{R}) in this language is decidable (in particular, Euclidean geometry is decidable), and that all models of the theory of real-closed fields are elementarily equivalent.


The entire theory of o-minimal structures can be viewed as a vast extrapolation stemming from the Tarski-Seidenberg theorem and its consequences.

Not all the extrapolations are based on quantifier elimination, but practically all do involve some reduction of logical complexity of formulas. An example is Wilkie’s theorem on the structure of the ordered exponential field \mathbb{R} (in the language (0,1,+,,exp,<)(0, 1, +, \cdot, \exp, \lt) where exp\exp is interpreted as the usual exponential function exp(x)=e x\exp(x) = e^x):


(Wilkie) Any subset of m\mathbb{R}^m definable in the language of ordered exponential fields can be defined by means of an existential formula

x m+1x nf 1(x 1,,x n,e x 1,,e x n)==f r(x 1,,x n,e x 1,,e x n)=0\exists x_{m+1}\ldots\exists x_n \, f_1(x_1,\ldots,x_n,e^{x_1},\ldots,e^{x_n})=\cdots= f_r(x_1,\ldots,x_n,e^{x_1},\ldots,e^{x_n})=0

where the f if_i are polynomials.

Here the critical point is that the complement of a set defined by such an existential formula is definable by another such existential formula. This is called a model completeness result, and it implies that an alternating string of quantifiers =¬¬,\forall = \neg \exists \neg, \exists can be eliminated in favor of just existential quantifiers at the head of a defining formula.


It is not known whether the theory of ordered exponential fields is decidable, but it is known that such decidability follows if one assumes Schanuel's conjecture.

Last revised on July 15, 2013 at 00:01:59. See the history of this page for a list of all contributions to it.