Classifying the $n$-types over $(\mathbb{Z}, S)$

Question

Consider the structure $(\mathbb{Z}, S)$, where $S$ is the successor function. I'm trying to work out a classification of the $n$-types over it, and would appreciate some help in how to go about it.

The $1$-types are, I think, rather simple: they are either isolated by $v = a$ for some $a \in \mathbb{Z}$ or equal to $p = \{v \not = a \; | \; a \in \mathbb{Z}\}$, the only non-isolated type.

But what about $n$-types for $n > 1$? The $2$-types seem to be of the form $v_1 = a \wedge v_2 = b$ and $v_1 = a \vee v_2 = b$ for $a, b \in \mathbb{Z}$, $p = \{v_1 \not = a \wedge v_2 \not = b \; | \; a,b \in \mathbb{Z}\}$, and $p =\{v_1 \not = a \wedge v_2 = b \; | \; a \in \mathbb{Z}\}$ for fixed $b$, as well as similar types with the order of the conjuncts changed or with the conjunction exchanged for a disjunction. Is that it? If so, are $n$-types in general just conjunctions and disjunctions of this sort? Is there a principled way to go about this?

Answer 1

Aside from the types isolated by $v_1 = a \land v_2 = b$, none of the other types you listed are complete $2$-types. For example, $\{v_1\neq a \land v_2\neq b \mid a,b\in \mathbb{Z}\}$ doesn't decide the truth value of the formula $v_1 = v_2$, or of $S(v_1) = v_2$.

The $2$-types in this structure are described as follows:

• $v_1 = a$ and $v_2 = b$, for $a,b\in\mathbb{Z}$.
• $v_1 = a$, for $a\in \mathbb{Z}$, and $v_2\notin \mathbb{Z}$.
• $v_2 = b$, for $b\in \mathbb{Z}$, and $v_1\notin \mathbb{Z}$.
• $v_1,v_2\notin \mathbb{Z}$, and one of the following holds: (a) $v_1 = v_2$, (b) $v_1 = S^n(v_2)$ for $n>0$, (c) $S^n(v_1) = v_2$ for $n>0$, (d) none of the above.

The above cases are obviously mutually exclusive. You can prove that they determine complete types by showing that any two pairs in the same case have the same type, by (1) EF games, or (2) by showing they're conjugate by an automorphism in an elementary extension, or (3) by proving quantifier elimination and showing that the information in each of these cases determines the truth of every quantifier-free formula.

Perhaps a more principled way to go about this, if you're not sure how to guess the complete types above, is to prove quantifier elimination, describe all the atomic formulas with parameters from $\mathbb{Z}$, and then think about the implications between quantifier-free formulas.