This theorem says that quantifiers over real variables can be eliminated from classical first order formulae built from equations and inequalities between polynomials with rational coefficients, ie in a language with ${=},{\leq},{\geq},{\neq},{<},{>},{\land},{\lor},{\lnot},{\Rightarrow}$ and $\forall x:{\mathbb R}$ and $\exists x:{\mathbb R}$.
Is there a similar result for just ${\neq},{<},{>},{\land},{\lor}$ and $\forall x:[a,b]$ and $\exists x:[a,b]$, ideally a constructive proof?
I am asking this towards the research goal of having a feasible way of computing Cauchy sequences from Dedekind cuts.
The research question is a conspicuous gap in the research community that I describe below, so since the answer to the textbook question above seems to be yes, I would like to invite semi-algebraic geometers to join that community.
The book
*Algorithms in real algebraic geometry*
by Saugata Basu, Richard Pollack and Marie-Françoise Roy
(Springer 2006)
is [freely and legally available online](https://perso.univ-rennes1.fr/marie-francoise.roy/bpr-ed2-posted1.pdf).
It looks very well written and relevant to this question, albeit classically, but Remark 3.2 comes tantalisingly close without answering it.
My language
===========
I am interested in the following language of predicates on ${\mathbb R}^n$,
which I am calling **bounded**:
* $f(x_1,...,x_k) > 0$, or $< 0$, or $\neq 0$, where $f$ is a polynomial in real variables but
rational coefficients and the **inequality is strict**,
so $=$, $\leq$ and $\geq$ are not allowed;
* finite conjunction and disjunction, but **not negation or implication**; and
* universal and existential quantification of any real variable
over **bounded closed** intervals, not the whole real line.
Context
=======
These predicates define **open** subspaces. They are a fragment of my
[*Lambda Calculus for Real Analysis*](http://paultaylor.eu/ASD/lamcra).
Any bounded predicate has a **partner** obtained as a "de Morgan dual",
ie by switching
$$ >/<,\quad \top/\bot,\quad \min/\max,\quad \sup/\inf,\quad \land/\lor,\quad \forall/\exists. $$
For example, let $f(x)$ be a polynomial with one variable and one real root
that increases from $-\infty$ to $+\infty$. Then the subsets
$$ D = \{ x : f(x) < 0 \} \quad\mbox{and}\quad U = \{ x : f(x) > 0 \} $$
form a **Dedekind cut**, ie
* $D$ is lower and $U$ is upper;
* they are rounded (open), ie $\forall d\in D.\exists d'. d < d' \in D$;
* they are inhabited;
* they are disjoint; and
* they are **order located**, ie
$$ \forall d, u. d < u \Longrightarrow d\in D \lor u\in U $$
and **arithmetically located**, ie
$$ \forall \epsilon > 0. \exists d\in D. \exists u\in U. |u-d| \lt \epsilon. $$
(Beware that there is another meaning of *located* in constructive analysis
that says that the distance between two sets is a two-sided real number,
but this is not what I mean.)
The real number that $(D,U)$ represents is the root of the polynomial $f$.
Given another Dedekind cut $(E,T)$, confusing them both with their values,
$$ \min ( (D,U), (E, T) ) = ( (D \cap E), (E \cup T) ) $$
$$ \max ( (D,U), (E, T) ) = ( (D \cup E), (E \cap T) ) $$
Similarly, $\sup$ and $\inf$ correspond to $\bigcap$ and $\bigcup$,
although I prefer to write predicates $\delta(x,y)$ and $\upsilon(x,y)$
with $\forall$ and $\exists$:
$$ \inf \{ ( \delta(-,y), \upsilon(-,y) ) : y\in[a,b] \}
= ( \forall x:[a,b].\delta(x,y), \exists x:[a,b].\upsilon (x,y) ) $$
$$ \sup \{ ( \delta(-,y), \upsilon(-,y) ) : y\in[a,b] \}
= ( \exists x:[a,b].\delta(x,y), \forall x:[a,b].\upsilon (x,y) ) $$
Now consider a single polynomial inequality in one variable $f(x) > 0$,
but with any number of real roots.
There are finitely many open intervals where this is true
and another finite number of them where $f(x) < 0$ instead.
If $f$ has no repeated roots, the positive and negative intervals alternate
but otherwise they have single-point holes.
These two open sets are disjoint.
I can think of ways of saying that they are order- or arithmetically located
in the one-variable case, but **how can this be formulated for more variables?**
The behaviour is similar when we add in the (bounded) logical operations.
Dedekind cuts to Cauchy sequences
=================================
The predicates in my *Lambda Calculus* may involve $\exists x:{\mathbb R}$ and
$\exists x:{\mathbb N}$, which I am calling **unbounded**.
They still define open subsets of ${\mathbb R}^n$, but no longer with partners.
They can be expressed as a *directed* joins of bounded predicates.
I want to use these facts to obtain an algorithm for **translating Dedekind cuts**
(expressed as two predicates in my *Lambda Calculus*) **into Cauchy sequences**.
In the case of bounded predicates and their partners,
(the Interval version of) the Newton-Raphson algorithm can be used
to fill the two parts with polygons and so obtain fast-converging Cauchy sequences.
In the unbounded case, the one part can still be approximated, but possibly very slowly.
However, when there are two unbounded predicates forming a Dedekind cut,
the order-locatedness property can be used to force convergence.
The Tarski-Seidenberg theorem
==========================
When I asked about this on the
[*Constructive News* Google Group](http://groups.google.com/g/constructivenews/c/NKoRpwDA4MQ/m/L8VW-jS9AAAJ)
my attention was drawn to the **Tarski-Seidenberg** theorem.
That result is about **semi-algebraic sets**, in which
$=$, $\leq$, $\geq$, $\lnot$, $\Rightarrow$ and quantification over the whole real line
are also allowed.
[Alfred Tarski showed](http://www.rand.org/content/dam/rand/pubs/reports/2008/R109.pdf)
in 1948 that **quantifiers may be eliminated** from this (more general) language.
Some [lecture notes by Andrew Marks at UCLA](http://www.math.ucla.edu/~marks/6c/15.pdf)
sketch a proof of this. This was the only freely downloadable one that I could find,
so some other online references would be appreciated.
I have tried above to make it clear that I am interested in a more restricted language
than semi-algebraic sets,
but it is inevitable that discussion would be diverted to the Tarski-Seidenberg result.
So I will go with that:
**Can this theorem be adapted to my language with strict inequalities and bounded quantifiers?**
It is plausible, because my bounded predicates certainly do define open subsets.
As I have said, the reason why I am interested in this is to convert Dedekind cuts into
Cauchy sequences.
I am skeptical that model-theoretic quantifier elimination helps with this.
So, if there is a counterexample, it would focus future discussion on the system
that interests me.
On the other hand, there may be people who know about results like this
and could contribute to the main project.
Research Communities
====================
This is clearly an intellectual gap in the community to which I belong,
which contains theoretical constructive topologists and analysts on the one hand
and clever programmers doing "exact real" computation on the other.
This community recently had a conference in Padova called
[*Continuity, Computability, Constructivity: From Logic to Algorithms*](http://events.math.unipd.it/ccc2022/).
My suspicion is that there is another community, possibly that of Computer Algebra,
that would be able to fill this intellectual gap in ours.