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.

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 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? It is plausible, because my bounded predicates certainly do define open subsets.

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative. These (and the endpoints) provide the extreme values, so substituting them those the quantifier in favour of finite disjunctions or conjunctions. This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

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.

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.