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

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.

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$.