---
title: Natural Numbers with Successor
module: Number Theory and Definability
moduleNumber: 6
lessonNumber: 2
order: 602
summary: >
  The weakest reduct keeps only zero and successor. Its models are a standard
  chain together with disjoint copies of the integers, which makes the theory
  categorical in every uncountable power, hence complete and decidable. A
  quantifier-elimination procedure gives a practical decision method and shows a
  subset is definable if and only if it is finite or cofinite.
topics: [Number Theory and Definability]
sources:
  - book: Enderton
    ref: "Ch. 3 — Undecidability; §3.1 Natural Numbers with Successor"
draft: false
---

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](/logic/arithmetic-and-definability/definability-in-arithmetic)
all get complete answers. The reduct is

$$
\fN_S = (\mathbb{N};\ 0, S).
$$

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 $\fN_S$, turns out to axiomatize
the whole theory. Let $A_S$ consist of:

- **(S1)** $\forall x\ Sx \neq 0$ — zero has no predecessor.
- **(S2)** $\forall x\, \forall y\, (Sx = Sy \rightarrow x = y)$ — successor is
  one-to-one.
- **(S3)** $\forall y\, (y \neq 0 \rightarrow \exists x\ y = Sx)$ — every nonzero
  number is a successor.
- **(S4.$n$)** $\forall x\ S^n x \neq 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 S x$ with $n$ occurrences of $S$, so S4 is a **schema**: one axiom
  for every positive $n$, infinitely many in total.

Since $\fN_S$ satisfies every member of $A_S$, it is a model, so every
sentence in the
[consequence set](/logic/models-and-theories/theories-elementary-classes-and-categoricity)
$\Cn A_S = \{\sigma : A_S \models \sigma\}$ — everything true in
every model of the axioms — is true here:

$$
\Cn A_S \subseteq \Th\fN_S.
$$

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

## Models of the axioms

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

- **The standard part.** Starting at $0^{\fA}$ and applying
  $S^{\fA}$ generates distinct points
  $0^{\fA} \to S^{\fA}(0^{\fA}) \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}$.

$$
% caption: Every model of the successor axioms is one copy of the natural numbers
% (the standard part rooted at zero) plus any number of disjoint two-sided chains
% ordered like the integers.
\begin{tikzpicture}[>=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  % standard part
  \node[anchor=east, acc] at (-0.4,1.4) {standard part};
  \foreach \x/\n in {0/0, 1.5/1, 3.0/2, 4.5/3} {
    \fill[acc] (\x,1.4) circle (2.2pt);
    \node[below=2pt, font=\scriptsize] at (\x,1.4) {\n};
  }
  \foreach \d in {0,1,2} \fill[acc] (5.9+\d*0.16,1.4) circle (0.9pt);
  \foreach \a/\b in {0/1.5, 1.5/3.0, 3.0/4.5} \draw[->, acc, thick] (\a+0.12,1.4) -- (\b-0.12,1.4);
  \draw[->, acc, thick] (4.5+0.12,1.4) -- (5.6,1.4);
  % a Z-chain
  \node[anchor=east] at (-0.4,0) {Z-chain};
  \foreach \d in {0,1,2} \fill[black] (-0.35+\d*0.16,0) circle (0.9pt);
  \foreach \x in {0.6, 2.1, 3.6, 5.1} \fill[black] (\x,0) circle (2.2pt);
  \node[below=2pt, font=\scriptsize] at (3.6,0) {$a$};
  \node[below=2pt, font=\scriptsize] at (5.1,0) {$Sa$};
  \foreach \a/\b in {0.6/2.1, 2.1/3.6, 3.6/5.1} \draw[->, black, thick] (\a+0.12,0) -- (\b-0.12,0);
  \draw[->, black, thick] (0.1,0) -- (0.48,0);
  \draw[->, black, thick] (5.1+0.12,0) -- (5.9,0);
  \foreach \d in {0,1,2} \fill[black] (6.05+\d*0.16,0) circle (0.9pt);
\end{tikzpicture}
$$

Say two points are **equivalent** when $S^{\fA}$ can be applied finitely
many times to one to reach the other. This is an equivalence relation (reflexive
and symmetric immediately, transitive because $S^{\fA}$ is one-to-one).
Its classes are the standard part (the class of $0^{\fA}$) 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**.[^models]

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

$$
\card|\fA| =
\begin{cases}
\aleph_0 & \text{if } \fA \text{ has countably many Z-chains,} \\
\lambda & \text{if } \fA \text{ has uncountably many, } \lambda \text{ of them.}
\end{cases}
$$

The intended structure $\fN_S$ has zero Z-chains, but any number is
realized by some model.

> **Lemma (Isomorphism by Z-chain count).** If $\fA$ and
> $\fA'$ are models of $A_S$ with the same number of Z-chains, they are
> isomorphic.

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.[^models]

No sentence, and no set of sentences, can say "there are no Z-chains." By the
[Löwenheim–Skolem theorem](/logic/models-and-theories/compactness-and-lowenheim-skolem)
there is an uncountable structure $\fA$ elementarily equivalent to
$\fN_S$; that $\fA$ has uncountably many Z-chains while
$\fN_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](/logic/models-and-theories/theories-elementary-classes-and-categoricity).

> **Theorem (Categoricity in uncountable powers).** Any two uncountable
> models of $A_S$ of the same cardinality are isomorphic.

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.

> **Theorem (Completeness of the successor axioms).** $\Cn A_S$ is a complete theory.

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

> **Corollary (The successor axioms axiomatize the theory of the naturals with successor).** $\Cn A_S = \Th\fN_S$.

The theory $\Cn A_S$ is complete and contained in the satisfiable
theory $\Th\fN_S$; a complete theory has no consistent
proper extension, so the two coincide.

> **Corollary (Decidability of the successor theory).** $\Th\fN_S$ is
> decidable.

A theory that is both complete and axiomatizable is decidable, and $A_S$ is a
decidable set of axioms for it.[^complete] This answers question (A) for the
successor reduct: decidable, axiomatizable, but not by any finite set (Th
$\fN_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**

$$
\varphi(0) \rightarrow \forall v_1\, \bigl(\varphi(v_1) \rightarrow
\varphi(S v_1)\bigr) \rightarrow \forall v_1\, \varphi(v_1)
$$

for wffs $\varphi$ of this language with only $v_1$ free. Then $A_S \subseteq
\Cn A_S^\ast$, so $\Cn A_S^\ast =
\Th\fN_S$ as well: in this weak language, first-order
induction proves S3 and every no-loop axiom, and adds nothing beyond them.[^ind]

## 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.

> **Definition (Quantifier elimination).** A theory $T$ _admits elimination of
> quantifiers_ iff for every formula $\varphi$ there is a quantifier-free formula
> $\psi$ with $T \models (\varphi \leftrightarrow \psi)$.

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.

> **Theorem (Reduction of quantifier elimination to a primitive case).** If for every $\varphi$ of
> the form $\exists x\, (\alpha_0 \wedge \dots \wedge \alpha_n)$, with each
> $\alpha_i$ atomic or a negated atomic formula, there is a quantifier-free $\psi$
> with $T \models (\varphi \leftrightarrow \psi)$, then $T$ admits elimination of
> quantifiers.

$$
% caption: Quantifier elimination reduces any formula to the primitive case: push
% quantifiers inward, convert to disjunctive normal form, split the disjuncts, and
% discharge a single existential standing before a conjunction of literals.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  b/.style={draw, minimum width=25mm, minimum height=11mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[b] (any)  at (0,0)    {any formula};
  \node[b] (dnf)  at (3.5,0)  {disjunctive\\normal form};
  \node[b] (prim) at (7.2,0)  {single existential\\over literals};
  \node[b, draw=acc, text=acc] (qf) at (11.0,0) {quantif\/ier\\free};
  \draw[->, acc, thick] (any)  -- (dnf);
  \draw[->, acc, thick] (dnf)  -- (prim);
  \draw[->, acc, thick] (prim) -- (qf);
  \node[font=\scriptsize, anchor=south] at (1.75,0.62) {push inward};
  \node[font=\scriptsize, anchor=south] at (5.35,0.62) {split disjuncts};
  \node[font=\scriptsize, anchor=south] at (9.1,0.62)  {discharge};
\end{tikzpicture}
$$

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

> **Theorem (Quantifier elimination for the successor theory).** $\Th\fN_S$ admits elimination of
> quantifiers.

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 \dots
\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 \neq 0$. Two cases finish
it:[^qe]

- **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

$$
t \neq 0 \ \wedge\ \dots\ \wedge\ t \neq S^{m-1} 0
$$

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

$$
% caption: The primitive existential splits on whether any literal is a positive
% equation: with all literals negated the witness dodges finitely many values;
% one positive equation fixes the witness and substitution removes it.
\begin{tikzpicture}[>=stealth, font=\footnotesize,
  b/.style={draw, minimum width=32mm, minimum height=11mm, align=center}]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{grn}{HTML}{2E7D46}
  \node[b] (root) at (0,0) {existential over\\conjunction of literals};
  \node[b, draw=acc, text=acc] (neg) at (5.8,1.5)  {all literals negated};
  \node[b, draw=grn, text=grn] (pos) at (5.8,-1.5) {some equation positive};
  \node[b] (true) at (11.4,1.5)  {always solvable\\replace by truth};
  \node[b] (sub)  at (11.4,-1.5) {witness f\/ixed\\substitute and drop};
  \draw[->, acc, thick] (root) -- (neg);
  \draw[->, grn, thick] (root) -- (pos);
  \draw[->, acc, thick] (neg) -- (true);
  \draw[->, grn, thick] (pos) -- (sub);
\end{tikzpicture}
$$

> **Worked example (Eliminating a quantifier in the successor theory).** Take
> $\exists x\, (SSx = y \ \wedge\ x \neq z)$, which says $y$ is at least $2$ and
> its double predecessor differs from $z$. Case 2 applies, with $\alpha_0$ the
> equation $S^2 x = y$ (so $m = 2$, $t = y$).
> - **Replace $\alpha_0$ by the solvability guard.** $S^2 x = y$ has a solution
>   in $\mathbb{N}$ iff $y \notin \{0, 1\}$, so $\alpha_0$ becomes $y \neq 0
>   \wedge y \neq S0$.
> - **Raise the other literal to level $m$.** The literal $x \neq z$ negates
>   $S^0 x = S^0 z$. Prefixing $S$ twice on both sides (S2 makes this reversible)
>   gives $S^2 x = S^2 z$, and substituting $t = y$ for $S^2 x$ turns it into
>   $y = S^2 z$; the original negation becomes $y \neq S^2 z$.
> - **Drop the quantifier.** No occurrence of $x$ remains.
>
> The quantifier-free equivalent is
> $$
> y \neq 0 \ \wedge\ y \neq S0 \ \wedge\ y \neq SSz,
> $$
> which reads $y \ge 2$ and $y \neq z + 2$. Every elimination in this theory has
> this shape: a Boolean combination of equations between terms $S^k u$.

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 \neq l$; so $A_S$ decides $\tau$, hence $\sigma$.
Second, a decision method that is explicit rather than an appeal to a
metatheorem.

```algorithm
caption: $\textsc{Decide}_S(\sigma)$ — decide a sentence of $\Th\fN_S$
$\tau \gets$ quantifier-free formula with $A_S \models (\sigma \leftrightarrow \tau)$  // quantifier elimination for the successor theory
for each atomic sentence $S^k 0 = S^l 0$ occurring in $\tau$ do
  replace it by $\top$ if $k = l$, else by $\bot$
evaluate the resulting Boolean combination
return true if the value is $\top$, else false
```

> **Worked example (Deciding a sentence of $\Th\fN_S$).** Run
> $\textsc{Decide}_S$ on $\sigma = \exists x\, (SSx = SSSS0)$, which asserts $4$
> has a double predecessor. Quantifier elimination (Case 2, $m = 2$, $t = SSSS0$)
> replaces the equation by its solvability guard, with no other literal to raise:
> $$
> \tau \ =\ SSSS0 \neq 0 \ \wedge\ SSSS0 \neq S0.
> $$
> The two atomic sentences $S^4 0 = S^0 0$ and $S^4 0 = S^1 0$ are both false,
> since $4 \neq 0$ and $4 \neq 1$, so each negation evaluates to $\top$. The
> conjunction is $\top$, and $\sigma$ is a theorem of $A_S$. Replacing the target
> $SSSS0$ by $S0$ would make the guard $S0 \neq 0 \wedge S0 \neq S0$ evaluate to
> $\bot$: "$1$ has a double predecessor" is refuted, correctly.

## Definable subsets

Quantifier elimination also settles definability. Any formula with $v_1$ free is
equivalent in $\fN_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.

> **Theorem (Definable sets of $\fN_S$).** A subset of $\mathbb{N}$ is
> definable in $\fN_S$ iff it is finite or its complement is finite
> (finite or cofinite).

$$
% caption: The only definable subsets in the successor reduct are the finite sets
% and their complements; anything requiring an infinite set with an infinite
% complement, such as the even numbers, is undefinable here.
\begin{tikzpicture}[>=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \definecolor{grn}{HTML}{2E7D46}
  % finite set: members 1,4
  \node[anchor=east, font=\scriptsize] at (-0.3,1.2) {f\/inite};
  \foreach \x in {0,1,2,3,4,5,6,7,8} \draw[black] (\x*0.75,1.2) circle (2.6pt);
  \foreach \x in {1,4} \fill[grn] (\x*0.75,1.2) circle (2.6pt);
  \node[grn, anchor=west, font=\scriptsize] at (6.6,1.2) {def\/inable};
  % cofinite set: everything except 2,5
  \node[anchor=east, font=\scriptsize] at (-0.3,0.4) {cof\/inite};
  \foreach \x in {0,1,3,4,6,7,8} \fill[grn] (\x*0.75,0.4) circle (2.6pt);
  \foreach \x in {2,5} \draw[black] (\x*0.75,0.4) circle (2.6pt);
  \node[grn, anchor=west, font=\scriptsize] at (6.6,0.4) {def\/inable};
  % even numbers
  \node[anchor=east, font=\scriptsize] at (-0.3,-0.4) {even};
  \foreach \x in {1,3,5,7} \draw[black] (\x*0.75,-0.4) circle (2.6pt);
  \foreach \x in {0,2,4,6,8} \fill[acc] (\x*0.75,-0.4) circle (2.6pt);
  \node[acc, anchor=west, font=\scriptsize] at (6.6,-0.4) {not def\/inable};
\end{tikzpicture}
$$

The even numbers are neither finite nor cofinite, so they are undefinable in
$\fN_S$, and likewise the ordering relation $\{\langle m, n\rangle : m <
n\}$. Recovering order takes new vocabulary: the
[reduct with $<$](/logic/arithmetic-and-definability/presburger-and-reducts)
adds the ordering symbol and, later, addition, tracking how far definability and
decidability stretch before multiplication breaks them.

[^axioms]: Enderton, §3.1 — the axiom set $A_S$ (S1–S3 and the schema S4.$n$) and the inclusion $\Cn A_S \subseteq \Th\fN_S$.
[^models]: Enderton, §3.1 — every model of $A_S$ is a standard part plus disjoint Z-chains, the cardinality count $\aleph_0 + \aleph_0\cdot\lambda$, and Lemma 31A on isomorphism by Z-chain count.
[^complete]: Enderton, §3.1, Theorems 31B–31C and Corollaries 31D–31E — categoricity in uncountable powers, completeness by the Łoś–Vaught test, $\Cn A_S = \Th\fN_S$, and decidability.
[^qe]: Enderton, §3.1, Theorems 31F–31G — reduction of quantifier elimination to $\exists x$ over a conjunction of literals, and the elimination procedure for $\Th\fN_S$; the definability corollary is Exercises 4–5.
[^ind]: Enderton, §3.1, Exercise 1 — the axiom set $A_S^\ast$ of S1, S2, and the induction axioms satisfies $A_S \subseteq \Cn A_S^\ast$, hence $\Cn A_S^\ast = \Th\fN_S$; non-finite-axiomatizability is Exercise 6.