Consider the theory $\text{Th}(\mathbb{N}, S, 0)$, which we know to be axiomatized by the following axioms:
- $\forall x (S(x) \neq 0)$
- $\forall x \forall y (S(x) = S(y) \rightarrow x=y)$
- $\forall x (x \neq 0 \rightarrow \exists y (x=S(y))$
plus the axiom schema:
- $\forall x (S^n(x) \neq x)$ for each $n \in \mathbb{N}$ (where $S^n(x)$ is the aplication of $S$ $n$ times to $x$).
Now, it is well known that models of these theory are exactly those that have the form $\mathbb{N} + \lambda \cdot \mathbb{Z}$, where $\lambda$ is a finite or infinite cardinal. My question is about how to prove this. It is not difficult to show that any structure of this form is a model for the theory, but what about the converse, i.e. that any model of the theory has this form?
Now, it is clear that any model of this theory will consist of an initial segment which is a copy of $\mathbb{N}$. My thought was then to define an equivalence relation $x \equiv y$ iff there is $n$ such that $S^n(x)=y$, and then show that the equivalence classes will all be of the form $\mathbb{N}$ or $\mathbb{Z}$. Is this in the right direction?
Also, as a side note, just to check, but the $1$-types of this theory are all either isolated by a formula of the form $S^n(0)=x$, or else the unique non-isolated type $\{S^n(0) \neq x \; | \; n \in \mathbb{N}\}$, correct?
Best Answer
You've got the right idea, but it needs a tweak: the "finite distance" relation is what you want, but it's not what you've written (what you've written isn't symmetric). Set $x\sim y$ iff either there is some finite $n$ such that $S^n(x)=y$ or there is some finite $n$ such that $S^n(y)=x$ (note that this is just the usual "graph metric").
Now the key observations are that in any model of successor arithmetic there is exactly one element without a predecessor and the successor function is injective. These two facts quickly imply that any model of successor arithmetic consists of exactly one $\sim$-class of "type $\mathbb{N}$" and all other $\sim$-classes (if any) have "type $\mathbb{Z}$."
(It may help to think about what successor arithmetic proves about the "distance one" relation $x=S(y)\vee y=S(x)$; in my experience this is a bit easier to conceptualize, although I'm not sure why.)