An exercise on (isolated) types

Question

I am currently working through a model theory course and am doing some exercises from Marker's book. I am currently attempting exercise 4.5.2. Which states the following:

Let $T$ be the theory $(\mathbb{Z},s,<)$, where $s(x)=x+1$, i.e. the successor function. I am then asked to determine the types in $S_n(T)$, for all $n$. That means I have to find the complete types. The second part of the problem is then to figure out which of these types are isolated. There is only one example in Marker's book and it doesn't help me much with this problem. I find it hard to start just from the definition of a type.

Answer 1

The challenge here is to show that :

$T$ admits quantifiers elimination.

(Hint : try to axiomatize $\mathrm{Th}(\mathbb Z,<,s)$ ; show that the models of it [the axiomatization] are of the form $I \times \mathbb Z$ for $I$ a linear order ; then establish a back-and-forth between $\aleph_0$-saturated models [which is kind of easy once you know the form of the models] ; you then have quantifier elimination and completion ; completion assure that your axiomatization is indeed an axiomatization of $\mathrm{Th}(\mathbb Z,<,s)$.)

Then remark that $\mathbb Z$ is a substructure for any model of $T$ (namely if $i \in I$, $\mathbb Z \simeq \{i\} \times \mathbb Z$). By quantifier elimination, it is then an elementary subtructure. So $\mathbb Z$ is a prime model : in particular it is atomic and so realizes exactly the isolated types.

So one way to answer the question is to say that isolated types are those realized by $\mathbb Z$. You can even try to explicit them as the quantifier-free formula are very simple here.

Answer 2

A good way to approach figuring out what are the types is to remember that two elements are of the same type if and only if (the converse only works in homogeneous models such as the monster) there is a structure automorphism between them (make sure you understand why).

First try to understand what are the types of $(\mathbb{Z}, <)$:

Thus, given two tuples of distinct elements their type is reduced to asking what is the order relation between them, and how many elements come in between any two adjacent elements.

Thus, a realized type on $n$ variables $x_1,...,x_n$ which assures that $x_1,...,x_n$ are all different will always have a formula of the form $x_{\sigma(1)} < ... < x_{\sigma(n)}$ where $\sigma$ is a permutation on $1,...,n$.

A realized type which does not assure that all variables are different must contain formulae which tells us which variables are identified (or it would be partial). So an $n$-type with $m$ classes of variables (under the equivalence $x_i~x_j \iff x_i\doteq x_j \in p$) reduces to a type as described above on $m$ variables (this holds in the given theory, as there is no formula $\varphi(x,y)$ which can be solved both by a pair of unique elements and by the same element twice, this can be proven by induction on the complexity of the formula).

Having cleared that out we note that each of these types may be considered a partial type in $(\mathbb{Z},<,s)$ and we may ask how we may complete them.

The successor function allows you to determine the distance between two adjacent elements in the tuple without qauntifiers. So given, for example, a partial type which includes $x_{\sigma(1)}<...<x_{\sigma(1)}$ (which, by the above, determines it completely), it may be extended to include the formulae $x_{\sigma(i)} \doteq s^{n_i}(x_{{\sigma(1)}(i-1)})$ where $n_i$ are positive natural numbers, and these are the only ways to extend it so that it is realized. This in essence means that the realized types in the two theories are the same.

This does not only map all realized type, but demonstrates that they are all isolated by the formula which is the conjunction of the (finitely many) formulae we used above to characterize the types (another way to see it is to show that $\mathbb{Z}$ may be embedded in any model of this theory, and so all types realized in $\mathbb{Z}$ are realized in general, and so they have to be isolated by the omitting types theorem)

It remains to ask which types are omitted (remembering, of course, that isolated types may not be omitted, so these will be exactly the non-isolated types).

Recall that an omitted type is a collection of formulae with no element in $\mathbb{Z}$ which solves all of them, but such that any finite conjunction of them does have a solution.

EDIT: Anything below this point is blatantly wrong

This is impossible, though, as for any $n$ the map $k\mapsto n+k:\mathbb{Z}\to \mathbb{Z}$ is an isomorphism. This may be used to show that given an arbitrary collection of formulae, all of which have a solution, which are consistent with each other, we may find a tuple which solves all of them.

The bottom line is that all types are isolated.