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