# Is this fragment of arithmetic on $p^{-\infty} {\mathbb Z}$ decidable?

Let $p$ be a prime number. Consider the abelian group $p^{-\infty} {\mathbb Z} = \bigcup p^{-n} {\mathbb Z}$ consisting of rational numbers whose denominator is a power of $p$, under addition.

View ${\mathbb Z}$ as a predicate on $p^{-\infty} {\mathbb Z}$, in the sense that ${\mathbb Z}(x)$ is true if $x$ is an integer.

Let $\phi$ be the function from ${\mathbb Z}$ to $p^{-\infty} {\mathbb Z}$ given by $\phi(n) = p^n$.

Is the first order theory of $( p^{-\infty} {\mathbb Z}, =, >, 0, 1, +, {\mathbb Z}, \phi )$ decidable?

A bit of background: The theory of $({\mathbb Z}, =, >, 0, 1, +, \phi)$ is decidable (where here $\phi$ is restricted to natural numbers). This is a result of Semenov; see my answer to the question Beyond Presburger Arithmetic for more.

On the other hand, what I've described is pretty close to undecidable theories. If I included a predicate $f: {\mathbb Z} \times p^{-\infty} {\mathbb Z} \rightarrow p^{-\infty} {\mathbb Z}$ sending $(n,x)$ to $2^n \cdot x$, it would be undecidable by a result of Delon ("${\mathbb Q}$ Muni de l'Arithmetique Faible de Penzin est Decidable," Proc. of AMS, vol. 125, no 9, 1997).

Any references or results would be greatly appreciated.

-
I can't quite answer my own question, but I just found the paper "Describing Groups" by Andre Nies, in Bull. Symbolic Logic 13 (2007), no. 3. It seems like the theory $(p^{- \infty} {\mathbb Z}, =, +, 0)$ is decidable since it is "finite-automaton presentable" (FA-presentable). A quick guess is that the additional structure, $1$, ${\mathbb Z}$, and the predicate $\phi$ might also fit into the FA-presentable framework and give a proof of decidability. But I'd still apreciate the opinion of an expert! – Marty Sep 6 '12 at 22:13