Theory of successor ($T_S=\mathrm{Th}(\mathbb{N},s,0)$)

The complete theory of the standard successor structure is axiomatized by injectivity of $s$, $0$ outside its range, a predecessor for every nonzero element, and the sentences $s^n(x)\ne x$ for each positive integer $n$. Its models have a single distinguished one-sided chain generated by zero and any collection of two-sided integer chains. The classification of models of the successor theory proves completeness and explains why the theory is categorical at every uncountable cardinal but not at the countable cardinal.

In a model of the axioms for the theory of successor, repeatedly taking successor and predecessor partitions the domain into components. Injectivity and the predecessor axiom leave only the zero-generated one-sided chain and two-sided chains; the no-cycle axioms exclude finite components. Choosing one origin in each remaining component gives the displayed structure.

These axioms have quantifier elimination. To eliminate one existential quantification, put its quantifier-free matrix in disjunctive normal form. In a conjunction, an equality between a successor iterate of the bound variable and a parameter term fixes at most one candidate, by injectivity. Existence of the finitely many necessary predecessors excludes only finitely many initial zero iterates; the other equalities and inequalities then translate to conditions on the parameters by cancellation of successor iterates. If there is no such fixing equality, only finitely many candidates are excluded, so some point on the infinite zero chain works. Equalities between two different iterates of the same variable are false by absence of cycles. Thus the existential formula reduces to a quantifier-free formula.

Every closed quantifier-free sentence is decided by the distinct zero iterates, proving completeness. A one-variable formula over the empty set is a Boolean combination of finitely many equalities $x=s^n(0)$, modulo this theory. All points in added integer chains therefore realize the same nonisolated complete type over the empty set. At an uncountable cardinal $\kappa$ a model has exactly $\kappa$ integer components, proving categoricity there. A countable model with infinitely many integer components is an omega-saturated model because finite parameters involve only finitely many components, leaving a fresh one for every new-component type.