= Solution
Reuse the complete <free-bijection theory> from part (e). <Quantifier elimination> shows that every one-variable atomic statement is already decided by the no-finite-cycle axioms. Thus there is exactly one <complete one-type>, isolated by $x=x$.
For two <logical variables>, each <integer> $k$ gives a different <complete type> isolated by
$$
y=f^k(x).
$$
There is also the <complete type>
$$
p_\infty(x,y)=\{y\ne f^k(x):k\in\mathbb Z\},
$$
saying that the two elements lie in different orbits. These exhaust the possibilities by <quantifier elimination>. In particular
$$
\boxed{|S_1(T_{\mathbb Z})|=1,\qquad |S_2(T_{\mathbb Z})|=\aleph_0.}
$$
The last <complete type> is a <nonprincipal complete type>. Any <logical formula> uses only finitely many <integer> offsets after <quantifier elimination>; a pair in a single orbit with a sufficiently different offset agrees with a different-orbit pair on those tests. Hence no single <logical formula> can isolate $p_\infty$.
The one-orbit <first-order model> $(\mathbb Z,f(n)=n+1,g(n)=n-1)$ omits $p_\infty$, while a two-orbit <first-order model> realizes it. This illustrates the <omitting types theorem> and shows concretely why finitely many <complete one-types> alone cannot replace the all-arities condition in Ryll-Nardzewski.
Back to article page
