Some conventions and notation

Throughout this thesis, $\mathbb {Z}$, $\mathbb {Q}$, and $\mathbb {R}$ will be used to denote the integer, rational, and real rings respectively. For the remainder of this section it will always be assumed that $F$ is in prenex form (see [Mishra(1993)] p. 356 for a discussion of converting an arbitrary formula to prenex form). Specifically, it will be assumed that

$$F = (Q_1 x_{k+1})(Q_2 x_{k+2}) \cdots (Q_{r-k} x_r)[ F'(x_1,\cdots , x_r) ] \ ,$$

where $Q_i \in \{\exists , \forall \}$ and $F'$ is a quantifier free formula.

For any $p \in \mathbb {Z}[x_1,\ldots , x_r]$, the level of $p$ is defined as the largest $i$ such that $deg_{x_i}(p) > 0$. If $P$ is a set of polynomials, $P_i$ will denote the $i$-level elements of $P$.

Finally, the ``$\vert$'' symbol will be used to denote evaluation, so if $\alpha$ is a point in free-variable space, $F\vert _\alpha$ means $F$ evaluated at $\alpha$, as discussed in the previous section.