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 hold at the point $a$.

Throughout this ball we now have, much more simply,
$$ \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 is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

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?**