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$, 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. $$

In the case of a single inequality for a polynomial with exactly one root,
the predicate and its partner form a **Dedekind cut**
(they are upper/lower, rounded (open), inhabited, disjoint and located)
and the value of this cut is the root of the polynomial.

In the general case, the two predicates are still open and disjoint.
I would like to know how to state that they are also **located**
(in the sense of Dedekind cuts, ie they "touch",
not the one in constructive analysis that is based on distance).
The many-variable case is the difficulty.

Moreover, any predicate in my *Lambda Calculus* can be expressed as a *directed*
join of bounded ones.

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.