Quantifier Elimination for the theory of hyperreals with a much less than relation

Question

We define a binary predicate $\ll$ over hyperreals as follows: $x \ll y$ if for every positive standard real number $r$, we have that $0 \le rx < y$.

Now consider the first-order theory of true statements about the hyperreals in the language of real closed fields, plus this new symbol. Does this language admit quantifier elimination?

Answer 1

The answer is yes!

We will show how to eliminate the quantifier in $\exists x. L$, where $L$ is a conjunction of literals. This will imply that all formulas in the language admit quantifier elimination.

To do this, we will first introduce $\Gamma$, a new quantifier. $\Gamma r. \phi(r)$ is defined as $\exists q \in \mathbb R. \forall r \in \mathbb R. r > q \implies \phi(r)$, where $q$ is a variable not free in $\phi$; (note that $\mathbb R$ refers to the set of standard real numbers). That is, $\Gamma r. \phi(r)$ is true iff $\phi$ is true for arbitrarily large standard real numbers $r$.

Let $r$ and $r'$ be distinct variables other than $x$ that are not free in $L$. We define $L'$ as follows. Conjuncts of the form $s \ll t$ in $L$ are replaced by $0 \le s \land rs < t$. Conjuncts of the form $\lnot (s \ll t)$ are replaced by $0 > s \lor r's \ge t$. All other conjuncts are left as is.

$\exists x. L$ implies $\Gamma r'. \Gamma r. \exists x. L'$, because $s \ll t$ implies $0 \le s \land rs < t$ and $\lnot (s \ll t)$ implies $0 > s \lor r's \ge t$ for all standard real numbers $r$ and $r'$.

Conversely, $\Gamma r'. \Gamma r. \exists x. L'$ implies $\exists x. L$: let $H$ be an infinite hyperreal. As a real formula, if $\exists x. L'$ has an integer solution for $r$ less than some real, it has a maximal such solution. Therefore, by transfer, if $\exists x. L'$ has a hyperinteger solution $r$ less than some hyperreal, in this case $H$, it has a maximal such solution. By the assumption, there is a standard real $r'$, say $R'$, such that $\exists x. L'$ is true for arbitrarily large standard $r$. This includes arbitrarily large standard integers $r$, so $\exists x. L'$ does have an integer solution. Since integers are also hyperintegers, this implies $\exists x. L'$ has a maximal hyperinteger solution for $r$, say $R$. $R$ must be infinite, since it is larger than any of the integer solutions (which can be arbitrarily large standard integers). So for $r' = R'$ and $r = R$, there is $x$ that makes $L'$ true. This same $x$ is the witness for $\exists x. L$, since $0 \le s \land Rs < t$ implies $s \ll t$, and $0 > s \lor R's \ge t$ implies $\lnot(s \ll t)$.

Let $\psi$ be the quantifier elimination of $\exists x. L'$ (which exists since $L'$ is a formula in the language of RCF). Now we just need to eliminate quantifiers from $\Gamma r'. \Gamma r. \psi$.

Write the terms of $\psi$ as polynomials of $r$ and $r'$ (with the coefficients being terms not involving $r$ or $r'$). Literals of the form $p = 0$ (for polynomial $p$) are true iff all the coefficients are $0$. For literals of the form $p > 0$, we first introduce an ordering on the terms of $p$. $cr^n{r'}^m$ is a more significant than $dr^j{r'}^k$ iff:

• $|d| \ll |c|$ (because then $cr^n{r'}^m$ will always overwhelm $dr^j{r'}^k$, for any standard reals $r$ and $r'$)
• OR $\lnot (|c| \ll |d|)$ and $n > j$ ($cr^n{r'}^m$ can overwhelm $dr^j{r'}^k$ by taking large enough $r$, as a function $r'$)
• OR $\lnot (|c| \ll |d|)$ and $n = j$ and $m > k$ ($cr^n{r'}^m$ can overwhelm $dr^j{r'}^k$ by taking large enough $r'$, regardless of the value of $r$)

This is a total ordering of the terms. So $p > 0$ is true iff the most significant term of $p$ has a positive coefficient. That is because for arbitrarily large real $z$, the most significant term will be $z$ times larger in absolute value than the any of the other terms. So if there are less than $z$ other terms, the sign will be determined by the most significant term. The above procedure can be represented as a quantifier free formula not involving $r$ and $r'$. The formula is a disjunction, with a disjunct for each term. The disjunct says that the coefficient is positive and the term is more significant than each of the other terms. The resulting formula is a length of $O(n^2)$, where $n$ is the number of terms. Replacing each literal in $\psi$ with a quantifier free formula this way, we arrive at $\psi'$ that is equivalent to $\Gamma r'. \Gamma r. \psi$.

So $$\exists x. L \equiv \Gamma r'. \Gamma r. \exists x. L' \equiv \Gamma r'. \Gamma r. \psi \equiv \psi'$$

Q.E.D.

Note that this can also be used as an algorithm to decide sentences in the language. Once you eliminate quantifiers from a sentence, literals of the form $n \ll m$ are true if and only if $n = 0$ and $m > 0$. This is because there are no variables, and so $n$ and $m$ must be standard integers.