The theory of real closed fields is decidable. The [hyperreals](https://en.wikipedia.org/wiki/Hyperreal_number) 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?



Decidability of a first-order theory of hyperreals
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](https://doi.org/10.2307/2275510). On [JSTOR](https://www.jstor.org/stable/2275510).


[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](https://doi.org/10.1016/0168-0072(83)90019-2).


