Quantifier elimination for $\mathbb Z$ as a group?

Question

Question 1: What definable sets should one add to the language to obtain quantifier elimination for the theory of $(\mathbb Z, +)$, i.e. the integers as a group (short of simply Morleyizing)?

An $\omega$-saturated model is given by $\hat{\mathbb Z} \oplus {\mathbb Q}^{\oplus \omega}$. This can be seen by showing that if a constant for 1 is added to the language, then after defining negation and $n | x := \exists y (ny = x)$ for each $n \in \mathbb N$, one can perform a back-and-forth argument for the structure $(\hat{\mathbb Z} \oplus {\mathbb Q}^{\oplus \omega}, 0, 1, + , -, (n|)_{n \in \mathbb N})$ (where $1$ is interpreted as $1 \in \hat{\mathbb Z}$), so that this structure eliminates quantifiers; it is easy to see that it realizes all quantifier-free types, so it is $\omega$-saturated. Taking a reduct, $\hat{\mathbb Z} \oplus {\mathbb Q}^{\oplus \omega}$ is $\omega$-saturated in the group language.

However, $1$ is not definable in $(\mathbb Z, +)$, so this doesn't tell us how to obtain quantifier elimination in a definitional extension of the group language. A related puzzle is

Question 2: What is a model of the theory of $(\mathbb Z,+)$ which omits the type of $1$?

Answer 1

The complete theory of the structure $(\mathbb{Z}; 0,+,-,(n|)_{n\in \mathbb{Z}})$ , which is a definitional expansion of $(\mathbb{Z};+)$, has quantifier elimination. Of course, it already suffices to include the divisibility predicates $(p^k|)$ when $p$ is prime and $k>1$, since $n\mid x$ is equivalent to the conjunction of $p^k\mid x$ for each prime power $p^k$ dividing $n$.

This theorem is actually true for all abelian groups (and certain other modules, see below), with $n\mid x$ interpreted as $\exists y\, ny = x$ for $n\in \mathbb{Z}$. In this generality, it is due to Wanda Szmielew. From the modern perspective, it is a special case of the general quantifier elimination theorem for modules, which I believe is due to Walter Baur. You can find a short proof in Section 3.3.3 of A Course in Model Thoery by Tent and Ziegler. I'll state the result here:

Let $R$ be a ring (with $1$, but not necessarily commutative). Let $M$ be an $R$-module, viewed as a structure $(M;0,+,-,(r)_{r\in R})$, where $r$ is the symbol for multiplication by $r$.

An equation is a formula of the form $\gamma(\overline{x},\overline{y}):$ $$r_1x_1 + \dots + r_nx_n = r_1'y_1 + \dots + r_m'y_m$$ with all coefficients $r_i$ and $r_j'$ in $R$. A positive primitive formula (pp-formula) is one of the form $\varphi(\overline{x})$: $$\exists \overline{y}\,\bigwedge_{k = 1}^N \gamma_k(\overline{x},\overline{y}),$$ where each $\gamma_k$ is an equation.

Theorem: Relative to the complete theory of $M$, every formula is equivalent to a Boolean combination of pp-formulas.

An immediate consequence of this theorem is that the complete theory of the structure $(M;0,+,-,(r)_{r\in R},(P_A)_{A\in M(R)})$ has quantifier elimination. Here $P_A$ is an $m$-ary relation symbol for each $(m\times n)$ matrix $A$ with entries in $R$. It is interpreted by $M\models P_A(\overline{x})$ if and only if there is a vector $\overline{y}\in M^n$ such that $A\overline{y} = \overline{x}$.

Now it takes a little bit of linear algebra work to reduce the $P_A$ relations to the $(n|)$ relations in the case of abelian groups ($\mathbb{Z}$-modules). In the case of a pp-formula involving a single equation $\exists \overline{y}\, \gamma(\overline{x},\overline{y})$, this formula is equivalent to $(n\mid (r_1x_1+\dots r_nx_n))$ for some $n\in \mathbb{Z}$, simply because $\mathbb{Z}$ is a PID. But a general pp-formula involves a conjunction of equations with the same variables, which makes things a bit more complicated - the main trick is a diagonalization procedure. A reference is Section 2.$\mathbb{Z}$ of Model Theory and Modules by Mike Prest.

Extensions of this reduction argument were carried out for modules over PIDs by Eklof and Fisher, and for torsion-free modules over Bezout domains by van den Dries and Holly. In each of these cases, we get the theorem that the complete theory of $(M;0,+,-,(r)_{r\in R},(r|)_{r\in R})$ has quantifier elimination.

---

I haven't thought carefully about your second question, but here's an idea. First: the fact that $1$ is not definable in $(\mathbb{Z};+)$ doesn't immediately imply that there is a model of $\text{Th}(\mathbb{Z};+)$ omitting the type of $1$. What you really need to know is that the type of $1$ is not isolated by a single formula. But once you know the quantifier elimination result above, this is not hard to see: the complete type $p(x)$ of $1$ is axiomatized by the formulas asserting that $x$ is not divisible by any prime, and no finite set of these formulas suffice to imply the rest.

Ok, so we know that the embedding of $\mathbb{Z}$ into $\widehat{\mathbb{Z}}$ is elementary. What if we look at the subset of $\widehat{\mathbb{Z}}$ consisting of those elements which are divisible by all but finitely many primes? This is a subgroup, and it preserves the truth of all the $(n|)$ predicates, so if it is elementarily equivalent to $\mathbb{Z}$, then it is an elementary subgroup, and it doesn't contain an element realizing the type of $1$.

Part of Szmielew's work is a classification of abelian groups up to elementary equivalence by certain elementary invariants; for example, we get an explicit axiomatization of $\text{Th}(\mathbb{Z},+)$, which could be used to check that my proposed example works. The axioms are probably quite easy to state in the case of $(\mathbb{Z},+)$, but I've never actually read up on the details. A better (and easier to find!) reference than Szmielew's original paper is The elementary theory of Abelian groups by Eklof and Fisher.

Answer 2

In his answer, Alex Kruckman points out the excellent reference: Eklof and Fischer, The elementary theory of abelian groups. Let me just spell out what can be gleaned from this. They recover Szmielew's result that any abelian group $A$ is characterized up to elementary equivalence by the following four families of elementary invariants:

1. The torsionfree invariants $Tf(p; A) := \lim_{n \to \infty} \operatorname{dim}_{\mathbb F_p}(\frac{p^n A}{p^{n+1} A})$;

2. The order invariants $D(p; A) := \lim_{n \to \infty} \operatorname{dim}_{\mathbb F_p}((p^n A)[p])$;

3. The global order invariant $Exp(A)$, which is $0$ if $A[n] = A$ for some $n$ and $\infty$ otherwise;

4. The Ulm invariants $U(p,n;A) := \operatorname{dim}_{\mathbb F_p}(\frac{(p^n A)[p]}{(p^{n+1} A)[p]})$.

Here $p$ ranges over primes, $n \in \mathbb N$, and $B[n] = \{b \in B \mid nb = 0\}$ is the $n$-torsion of an abelian group $B$.

This simplifies nicely for us because in a torsionfree group, only the torsionfree invariants are nontrivial, and moreover the limit in the definition of the torsionfree invariant stabilizes at $n=0$. Thus the theory of $(\mathbb Z,+)$ is the theory of a torsionfree abelian group $A$ such that $A / p \cong \mathbb Z/p$ for each prime $p$.

It follows, then, along with the quantifier elimination results, that if $A$ is a model of the theory of $\mathbb Z$ and $B \subseteq A$ is any pure subgroup (i.e. a subgroup with the same $n$-divisibility relation as $A$ has for each $n$) which is not $p$-divisible for any $p$, then $B$ is an elementary subgroup of $A$ (the reasoning is that if $B/p = 0$, then $B$ is $p$-divisible, while if $B/p$ is bigger than $A/p$ then purity is contradicted). In particular, Alex's example of a subgroup of $\hat {\mathbb{Z}}$ omitting the type of $1$ is indeed a model of the theory of $\mathbb Z$.