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.

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 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 in 1948 that quantifiers may be eliminated from this (more general) language.

Some lecture notes by Andrew Marks at UCLA 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.

My suspicion is that there is another community, possibly that of Computer Algebra, that would be able to fill this intellectual gap in ours.