Classification of models of the successor theory
ID: classification-of-models-of-the-successor-theory
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 , modulo this theory. All points in added integer chains therefore realize the same nonisolated complete type over the empty set. At an uncountable cardinal a model has exactly 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.
New to topics? Read the docs here!