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.
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 >/<,\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.
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.
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?**
If there are no free variables then quantifying one of them is equivalent
to conjunction or disjunction over the finitely many extreme points of the polynomial,
which are roots of its second derivative.
**How can this be done when these extreme points are functions of free variables?**
It is plausible that the T-S theorem can be adapted, because my bounded predicates
certainly do define open subsets.
If there is a counterexample, it would help me focus future discussion on the system
that interests me.
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 would do this.
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.