= Solution
Consider the <partial type>
$$
p_\infty(x)=\{x\ne s^n(0):n\in\mathbb N\}.
$$
Each finite fragment is realized by a sufficiently large standard <natural number>, so it is consistent. It is omitted in the standard <successor structure>, since each of its elements equals one of the named iterates.
There is exactly one <complete type> extending this <partial type>. By <classification of models of the successor theory> and its quantifier-elimination property, a parameter-free one-variable formula is equivalent to a Boolean combination of finitely many equalities $x=s^n(0)$ and sentences whose truth is fixed by the theory. For a point on an extra integer chain every displayed equality is false, so all such points have the same <complete type>. Thus
$$
\boxed{\operatorname{tp}(z/\varnothing)\text{ for a point }z\text{ on an added integer chain}}
$$
is the required omitted <complete type>. More formally take all formulas true at such a point; $p_\infty$ axiomatizes that type modulo the theory, and its deductive closure is complete.
Back to article page
