Natural Numbers with Successor

The full structure of arithmetic is undecidable, but its reducts need not be. The weakest reduct keeps zero and successor as its only non-logical symbols, and there the three questions of decidability, definability, and nonstandard models all get complete answers. The reduct is

The numerals $S^{k}0$ still name every point, but with no order, addition, or multiplication the expressible sentences are, from the viewpoint of arithmetic, without content. That poverty is what makes the theory tractable.

Axioms for the successor theory

A short list of sentences, all true in ${\mathfrak{N}}_S$, turns out to axiomatize the whole theory. Let $A_S$ consist of:

• (S1) $\forall xSx\ne 0$ — zero has no predecessor.
• (S2) $\forall x\forall y(Sx=Sy\to x=y)$ — successor is one-to-one.
• (S3) $\forall y(y\ne 0\to \exists xy=Sx)$ — every nonzero number is a successor.
• (S4.$n$) $\forall x{S}^{n}x\ne x$, for each $n=1,2,\dots$ — no point returns to itself after $n$ successor steps. Here $S^{n}x$ abbreviates the term $S\cdots Sx$ with $n$ occurrences of $S$, so S4 is a schema: one axiom for every positive $n$, infinitely many in total.

Since ${\mathfrak{N}}_S$ satisfies every member of $A_S$, it is a model, so every sentence in the consequence set$\text{Cn }{A}_S=\{\sigma :A_S\models \sigma \}$ — everything true in every model of the axioms — is true here:

The reverse inclusion is not obvious and is proved by analyzing every model of $A_S$, not just the intended one.¹

Models of the axioms

Let $\mathfrak{A}=(|\mathfrak{A}|;0^{\mathfrak{A}},S^{\mathfrak{A}})$ be any model of $A_S$. By S1, S2, and S3 the map $S^{\mathfrak{A}}$ is a bijection of $|\mathfrak{A}|$ onto $|\mathfrak{A}|\setminus \{0^{\mathfrak{A}}\}$: injective by S2, and everything except $0^{\mathfrak{A}}$ is hit by S3. By S4.$n$ there are no finite cycles. Two structural pieces follow.

• The standard part. Starting at $0^{\mathfrak{A}}$ and applying $S^{\mathfrak{A}}$ generates distinct points $0^{\mathfrak{A}}\to S^{\mathfrak{A}}(0^{\mathfrak{A}})\to \dots$, a copy of $\mathbb{N}$.
• Z-chains. Any point $a$ outside the standard part has a full two-sided orbit. Each nonzero element has a unique predecessor (existence by S3, uniqueness by S2), so $a$ has predecessors as well as successors, all distinct (no finite cycles), forming a copy of $\mathbb{Z}$.

Say two points are equivalent when $S^{\mathfrak{A}}$ can be applied finitely many times to one to reach the other. This is an equivalence relation (reflexive and symmetric immediately, transitive because $S^{\mathfrak{A}}$ is one-to-one). Its classes are the standard part (the class of $0^{\mathfrak{A}}$) and the Z-chains (one class each). Conversely, any structure built from one standard part and any collection of disjoint Z-chains satisfies $A_S$. So the models of $A_S$ are classified exactly by their number of Z-chains.²

The count controls cardinality. With $\lambda$ Z-chains the universe has ${\aleph }_0+{\aleph }_0\cdot \lambda$ points, which is $\max ({\aleph }_0,\lambda )$:

The intended structure ${\mathfrak{N}}_S$ has zero Z-chains, but any number is realized by some model.

The standard parts match by a unique isomorphism; a chosen bijection between the Z-chain sets pairs the chains, any two Z-chains are isomorphic, and combining all the pieces (using the axiom of choice) gives an isomorphism of the whole structures.²

No sentence, and no set of sentences, can say there are no Z-chains. By the Löwenheim–Skolem theorem there is an uncountable structure $\mathfrak{A}$ elementarily equivalent to ${\mathfrak{N}}_S$; that $\mathfrak{A}$ has uncountably many Z-chains while ${\mathfrak{N}}_S$ has none. Elementary equivalence does not detect the difference, so no first-order condition isolates the standard model.

Completeness and decidability

The classification by Z-chain count feeds straight into the Łoś–Vaught test.

An uncountable model of cardinality $\kappa$ has $\kappa$ Z-chains, since with uncountably many the chain count equals the cardinality. Two such models of the same cardinality have equally many Z-chains, so the Z-chain counting lemma applies.

$A_S$ is categorical in every uncountable power and has no finite models, so the Łoś–Vaught test gives completeness directly.³ The rest follows.

The theory $\text{Cn }{A}_S$ is complete and contained in the satisfiable theory $\text{Th }{\mathfrak{N}}_S$; a complete theory has no consistent proper extension, so the two coincide.

A theory that is both complete and axiomatizable is decidable, and $A_S$ is a decidable set of axioms for it.³ This answers question (A) for the successor reduct: decidable, axiomatizable, but not by any finite set (Th ${\mathfrak{N}}_S$ is not finitely axiomatizable, since no finite subset of $A_S$ captures every S4.$n$).

The infinite schema S4.$n$ can be traded for a different infinite schema. Let $A_S^{\ast }$ consist of S1, S2, and every induction axiom

for wffs $\phi$ of this language with only $v_1$ free. Then $A_S\subseteq \text{Cn }{A}_S^{\ast }$, so $\text{Cn }{A}_S^{\ast }=\text{Th }{\mathfrak{N}}_S$ as well: in this weak language, first-order induction proves S3 and every no-loop axiom, and adds nothing beyond them.⁴

Elimination of quantifiers

Decidability from the Łoś–Vaught test is abstract. A concrete decision procedure comes from quantifier elimination: mechanically rewriting any formula into an equivalent one with no quantifiers, whose truth is then read off directly.

The whole job reduces to a single hard case. Pushing quantifiers inward and converting to disjunctive normal form, it is enough to eliminate one existential quantifier standing in front of a conjunction of literals.

Applied to the successor theory, the primitive case can always be discharged.

In this language the only terms are $S^{k}u$ with $u$ a variable or $0$, and the only atomic formulas are equations. Consider $\exists x({\alpha }_0\wedge \cdots \wedge {\alpha }_q)$ where $x$ occurs in each ${\alpha }_i$. Each ${\alpha }_i$ is an equation $S^{m}x=S^{n}u$ (or its negation), with $u$ different from $x$, since $S^{m}x=S^{n}x$ trivially reduces to $0=0$ or $0\ne 0$. Two cases finish it:⁵

• All literals negated. The conjunction says $x$ avoids finitely many values, which some $x$ always can. Replace the formula by $0=0$.
• Some literal positive. Say ${\alpha }_0$ is $S^{m}x=t$ with $t$ free of $x$. The equation forces a value of $x$, so substitute $S^{k}t$ for $S^{k+m}x$ in every other literal, guard against a negative solution, and $x$ disappears.

In the positive case the guard matters: the solution of $S^{m}x=t$ is $t$ minus $m$, which exists in $\mathbb{N}$ only when $t$ is at least $m$. The replacement for ${\alpha }_0$ is therefore

(or $0=0$ when $m=0$), asserting the solution is not forced negative.

Two by-products fall out of the procedure. First, an independent proof of completeness: any sentence reduces to a quantifier-free $\tau$, built from atomic sentences $S^{k}0=S^{l}0$, and each such atomic sentence is proved by $A_S$ when $k=l$ and refuted when $k\ne l$; so $A_S$ decides $\tau$, hence $\sigma$. Second, a decision method that is explicit rather than an appeal to a metatheorem.

Definable subsets

Quantifier elimination also settles definability. Any formula with $v_1$ free is equivalent in ${\mathfrak{N}}_S$ to a quantifier-free one in $v_1$, and a quantifier-free condition on a single variable, built from equations $S^m{v}_1=S^{n}0$, can only pin $v_1$ to finitely many values or exclude finitely many.

The even numbers are neither finite nor cofinite, so they are undefinable in ${\mathfrak{N}}_S$, and likewise the ordering relation $\{⟨m,n⟩:m<n\}$. Recovering order takes new vocabulary: the reduct with $<$ adds the ordering symbol and, later, addition, tracking how far definability and decidability stretch before multiplication breaks them.