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

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 is a counterexample, it would help me focus future discussion on the system
that interests me.

It is plausible that the T-S theorem can be adapted, 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.

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.