The quantifier-elimination problem

Another important problem was exemplified in (6.12). Consider the set of all Tarski sentences of the form (6.9), which may or may not have free variables. Can an algorithm be developed that takes a Tarski sentence $\Phi$ and produces an equivalent quantifier-free formula $\phi$? Let $x_1,\ldots, x_n$ denote the free variables. To be equivalent, both must take on the same true values over ${\mathbb{R}}^n$, which is the set of all assignments $(x_1,\ldots,x_n)$ for the free variables.

Given a Tarski sentence, $(\ref{eqn:tarski})$, the quantifier-elimination problem is to find a quantifier-free formula $\phi$ such that

$$\Phi (x_1,\ldots, x_n) = \phi (x_1,\ldots, x_n)$$ (6.14)

for all $(x_1,\ldots, x_n) \in {\mathbb{R}}^n$. This is equivalent to constructing a semi-algebraic model because $\phi$ can always be expressed in the form

$$\phi (x_1,\ldots, x_n) = \bigvee_{i=1}^k \; \bigwedge_{j=1}^{m_i} \left( f_{i,j}(x_1,\ldots, x_n) \bowtie 0 \right),$$ (6.15)

in which $\bowtie$ may be either $<$, $=$, or $>$. This appears to be the same (3.6), except that (6.15) uses the relations $<$, $=$, and $>$ to allow open and closed semi-algebraic sets, whereas (3.6) only used $\leq$ to construct closed semi-algebraic sets for ${\cal O}$ and ${\cal A}$.

Once again, the problem is defined on ${\mathbb{R}}^n$, which is uncountably infinite, but an algorithm must work with a finite representation. This will be achieved by the cell decomposition technique presented in Section 6.4.2.