Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?