Non-isolated types of Presburger Arithmetic I want to show that there are $2^{\aleph_0}$ countable models of Presburger Arithmetic. Now, there is a (more or less) easy argument for this using the fact that every subset of $\mathbb{N}$ is coded by a non-standard number. Since there are $2^{\aleph_0}$ subsets of $\mathbb{N}$, we must have $2^{\aleph_0}$ non-standard numbers, and since we can take these coding elements to be elements of countable non-standard models, a simple counting argument shows that there must be $2^{\aleph_0}$ such models.
But I also wanted to try a different argument, counting the types of this theory---and I wanted to check if my argument is sound. In particular, if I could show that there are $2^{\aleph_0}$ non-isolated types, a combination of the compactness and omitting types theorems would give that for each such type, there is a model that realizes it while omitting all the other non-isolated types, whence I would have the desired result.
So in order to obtain as many such types, I began to think about systems of congruences. That is, we know that the relation $n \equiv_{p} m$ is expressible in Presburger Arithmetic. And it seems to me that, for a fixed $m$, one determines a type by considering whether or not $x \equiv_p m$ for each prime $p$.  Since there are $\aleph_0$ many primes and two options for each prime, it seems that there are $2^{\aleph_0}$ many types---if whether or not $x \equiv_p m$ is in general indepedent of whether or not $x \equiv_{p'} m$, that is.
So this is my first question:

Is it true that whether or not $x \equiv_p m$ is independent of whether or not $x \equiv_{p'} m$?

If yes, then my second question is:

How do I show that each such type is non-isolated (if indeed it is)?

And, of course, it would be nice to have confirmation that my general strategy is sound!
 A: Following up on the discussion in the comments, let's describe the complete $1$-types over the empty set relative to Presburger Arithmetic.
The theory $T = \text{Th}(\mathbb{N};+,0,1,<,(D_p)_{p\in \mathbb{P}})$ has quantifier elimiation, where $D_p$ is a unary predicate expressing divisibility by $p$, and $\mathbb{P}$ is the set of primes. Since this is a definable expansion of $(\mathbb{N};+)$, $T$ is essentially the same as Presburger Arithmetic, and types relative to Presburger Arithmetic are essentially the same as types relative to $T$.
For each $n\in \mathbb{N}$, there is a type $q_n(x)$ isolated by the formula $x = n$, where $n$ is the term $\underbrace{1+\dots+1}_{n\text{ times}}.$
Suppose $q(x)$ is type which is not equal to $q_n(x)$ for any $n$. Note that it is quite clear that each such type $q(x)$ is non-isolated, since it is omitted in the standard model $\mathbb{N}$!
We have that $n < x$ is in $q(x)$ for all $n$. For each $p\in \mathbb{P}$, and each $0\leq m < p$, we can express $x\equiv_p m$ by $D_p(x+(p-m))$, and there is exactly one $m$ such that $x\equiv_p m$ is in $q(x)$. Now you should convince yourself that the truth value of any atomic formula in one free variable $x$ is determined by the above data, so that (by quantifier elimination) $q(x)$ is uniquely determined by a family of residues modulo each prime.
Conversely, suppose $(m_p)_{p\in \mathbb{P}}$ is a family of residues, with $0\leq m_p < p$ for all $p$. We would like to show that $$\{n < x\mid n\in \mathbb{N}\}\cup \{x\equiv_{p} m_p\mid p\in \mathbb{P}\}$$
is consistent. This follows directly from compactness and the Chinese remainder theorem. Indeed, a finite subset of this type is equivalent to $$\{N < x, x \equiv_{p_1} m_{p_1},\dots, x \equiv_{p_k} m_{p_k}\}$$ for some $N,k\in \mathbb{N}$ and $p_1,\dots,p_k\in \mathbb{P}$. By CRT, letting $M = \prod_{i=1}^k p_i$, there is some $0\leq m \leq M$ such that $m\equiv_{p_i} m_{p_i}$ for all $1\leq i\leq k$. Now picking $\ell$ large enough so that $N < \ell M$, these finitely many formulas are satisfied by $m + \ell M$ in $\mathbb{N}$.
This establishes that there are $2^{\aleph_0}$-many types: one isolated type for each natural number and one non-isolated type for each family of residues. As I pointed out in the comments, if you just want to count models, which types are isolated is irrelevant: any countable model realizes only countably many types, so if there are $2^{\aleph_0}$-many types, there must be $2^{\aleph_0}$-many models.

In the comments, we discussed the fact that realizing some non-isolated type sometimes forces you to realize others. This certainly happens in this example.
Suppose $a$ is a non-standard element of a countable model such that $a\equiv_{p} 0$ for all $p\in \mathbb{P}$. Then $a+1\equiv_{p} 1$ for all $p\in \mathbb{P}$, $a+2\equiv_p 2$ for all $p\in \mathbb{P}$, etc. Similar behavior happens for any non-isolated type relative to Presburger arithmetic: the non-isolated types come in countably infinite families, where realizing any type in the family forces you to realize all the others.
To help explain what's going on here: Let $q(x)$ be the non-isolated type determined by $x\equiv_{p} 0$ for all $p\in \mathbb{P}$, and let $r(y)$ be the non-isolated type determined by $x\equiv_{p} 1$ for all $p\in \mathbb{P}$. To ensure that we realize $q(x)$, we can introduce a new constant symbol $c$ and look at that $L(c)$-theory $T\cup q(c)$. Now there is a complete $L(c)$-type $r'(y)$ which is isolated by $y = c+1$ and whose reduct to $L$ is $r(y)$. Since $r'(y)$ is isolated, it must be realized in any model of $T\cup q(c)$. This shows that $r(y)$ must be realized in any model realizing $q(x)$.
