Decidability of a first-order theory of hyperreals

Question

The theory of real closed fields is decidable. The hyperreals satisfy that theory, so we can interpret statements in the theory of real closed fields as being about hyperreals.

If we add a unary predicate for "is a standard real number" to the language, is the theory still decidable?

Answer 1

Yes, the theory is decidable.

If $F$ is an ordered field and $R\subseteq F$ a non-cofinal subfield, then $$O=\{x\in F:\exists u\in R\:(-u\le x\le u)\}$$ is a convex valuation ring of $F$, with maximal ideal $$I=\{x\in F:\forall u\in R_{>0}\:(-u\le x\le u)\}.$$ $R$ embeds as a cofinal subfield in the residue field $O/I$; in general, the embedding may be proper, but if $R=\mathbb R$, then $R=O/I$, as $\mathbb R$ is complete.

Thus, let $T$ be the theory of structures $(F,R,+,\cdot,<)$ such that

1. $F$ is a real-closed field,

2. $R$ is a non-cofinal subfield of $F$, and

3. the canonical embedding of $R$ into the residue field $O/I$ as defined above is surjective (and therefore an isomorphism).

Then $T$ is a recursively axiomatized theory, it is valid in the hyperreal structures $({}^*\mathbb R,\mathbb R)$, and it is complete (see below), hence it is decidable, and axiomatizes the first-order theory of $({}^*\mathbb R,\mathbb R)$.

As pointed out in a comment by Erik Walsberg (thanks!), the completeness of $T$ is a special case of a more general result on tame elementary extensions of o-minimal structures due to Van den Dries and Lewenberg [1]. (Here, tameness is basically the axiom 3 above.) Their results also show that $T$ is model-complete, and in fact, that it has quantifier elimination in a language expanded with function symbols for roots of polynomials (which make the theory of real-closed fields universally axiomatized) and for the “standard part” map $\mathrm{st}\colon O\to R$ such that $x-\mathrm{st}(x)\in I$.

Let me indicate how to prove a weaker result: the theory $T_0$ of structures $(F,O)$ such that

1. $F$ is a real-closed field,

2. $O$ is a proper convex subring of $F$,

is complete and decidable. This follows from the Ax–Kochen–Ershov principle, which states that two henselian valued fields of residue characteristic $0$ with elementarily equivalent residue fields and value groups are elementarily equivalent.

First, it is an easy consequence of basic facts about valued fields that if $F$ is a real-closed field with a convex valuation ring $O$, then the valued field $(F,O)$ is henselian, the residue field $O/I$ is real-closed, and the value group $F^\times/O^\times$ is divisible.

Thus, if $(F,O)$ and $(F',O')$ are two models of $T_0$, their residue fields are elementarily equivalent by completeness of the theory of real-closed fields, and their value groups are elementarily equivalent by completeness of the theory of divisible totally ordered abelian groups, hence the valued fields $(F,O)$ and $(F',O')$ are elementarily equivalent by the AKE principle.

As shown by Cherlin and Dickman [2], $T_0$ has quantifier elimination in the language of ordered rings expanded with the predicate $$x\mid y\iff y\in xO.$$

References:

[1] Lou van den Dries, Adam H. Lewenberg: $T$-convexity and tame extensions, Journal of Symbolic Logic 60 (1995), no. 1, pp. 74–102, doi: 10.2307/2275510. On JSTOR.

[2] Gregory Cherlin, Max A. Dickmann: Real closed rings II. Model theory, Annals of Pure and Applied Logic 25 (1983), no. 3, pp. 213–231, doi: 10.1016/0168-0072(83)90019-2.

Answer 2

Here are some comments on quantifier elimination for this theory, focusing on what expansion of the language might make it work. This may be parallel to identifying a model companion, or determining the structures to consider in a more model-theoretic proof, as Emil Jerabek was proposing.

First, we will need a symbol for having a standard real in between, $SBet(x,y)$, to eliminate the quantifier in $$(\exists s)(Std(s)\ \&\ x \le s \le y)$$ We can express many things in terms of this symbol, e.g.

• $x$ is standard iff $SBet(x,x)$;
• $x$ is less than some standard real iff $x<0 \vee SBet(x,x+1)$;
• $x$ is in Emil's ideal $O$ iff $x$ and $-x$ are each less than some standard real

Second, we will need symbols for algebraic functions. We need to be able to say that $\sqrt{x}-y$ is standard, i.e. a quantifier elimination for expressions like $$(\exists r)(Std(r)\ \&\ (r+y)^2 = x)$$

• One obvious elimination does not work, e.g. if $x=(y+1)^2$ and $y$ is non-standardly large, then $\sqrt{x}-y$ is standard but $x-y^2$ is non-standard.

• Identifying algebraic functions by bracketing roots in rational intervals also will not work, since we will need roots that are not in rational intervals.

• We can instead use the sign representation, specifying the signs of the derivatives of the polynomial. So we add a function $a_d$ of $2d+1$ variables for each degree $d$, where we interpret, e.g. $a_2(c_0, c_1, c_2; d_1, d_2)$ as "the root of $c_0 + c_1 x + c_2 x^2$ for which $(c_0 + c_1 x + c_2 x^2)'$ has the same sign as $d_1$ and $(c_0 + c_1 x + c_2 x^2)''$ has the same sign as $d_2$, or $0$ if that description does not specify a unique $x$."

Even these additions don't make the quantifier elimination obvious. How can we eliminate the quantifier over $r$ in $$(\exists r)(SBet(r + x,\ r + 2x)\ \&\ y < r < z)\ \text{ or}$$ $$(\exists r)(SBet(r^3 - r + x,\ r^3 - r + 2x)\ \&\ y < r < z)\ ?$$