Tarski-Seidenberg for strict inequalities and bounded quantification

Question

This theorem says that quantifiers over real variables can be eliminated from classical first order formulae built from equations and inequalities between polynomials with rational coefficients, ie in a language with ${=},{\leq},{\geq},{\neq},{<},{>},{\land},{\lor},{\lnot},{\Rightarrow}$ and $\forall x:{\mathbb R}$ and $\exists x:{\mathbb R}$.

Is there a similar result for just ${\neq},{<},{>},{\land},{\lor}$ and $\forall x:[a,b]$ and $\exists x:[a,b]$, ideally a constructive proof?

I am asking this towards the research goal of having a feasible way of computing Cauchy sequences from Dedekind cuts.

The research question is a conspicuous gap in the research community that I describe below, so since the answer to the textbook question above seems to be yes, I would like to invite semi-algebraic geometers to join that community.

The book Algorithms in real algebraic geometry by Saugata Basu, Richard Pollack and Marie-Françoise Roy (Springer 2006) is freely and legally available online. It looks very well written and relevant to this question, albeit classically, but Remark 3.2 comes tantalisingly close without answering it.

My language

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.

Context

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

Dedekind cuts to Cauchy sequences

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.

The Tarski-Seidenberg theorem

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.

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.

Research Communities

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.

Answer 1

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where hold at the point $a$.

Throughout this ball we now have, much more simply, $$ \phi(x) \iff \bigvee_{i\in I} (p_i(x)=0), $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

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 eliminates 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?

Answer 2

EDIT(n+1):

I didn't see how this can work for universal quantifiers, as $(\forall y)(xy\neq 1)$ is equivalent to $(x=0)$.

Certainly, one must also impose $y_0\leq y\leq y_1$, for some $y_0<y_1$, to satisfy the condition that one cannot quantify over the whole real line. Then one gets $(1/y_0\lt x) \vee (x\lt 1/y_1)$, so this is not a counterexample, assuming $y_0>0$.

If $y_0y_1<0$, one sees that elimination gives $(1/y_0\lt x\lt 1/y_1)$, again all is fine.

In fact, as pointed out in the comments, this follows from a general result in topology due to Leopoldo Nachbin.