Peano Axioms

Why Peano axioms matter

• Foundation of arithmetic. The Peano axioms are the canonical starting point for formal arithmetic. Every proof in elementary number theory, when fully formalized, traces back to these five axioms plus first-order logic.
• Type theory and computer science. The successor function and recursion principle in Peano are direct ancestors of inductive types in modern proof assistants. Coq's Inductive nat := O | S (n : nat) is the type-theoretic translation of Peano.
• Formal verification. Hardware designers, cryptographers, and safety engineers rely on machine-checked proofs grounded in Peano arithmetic to verify that programs satisfy specifications.
• Reverse mathematics. The Friedman-Simpson program calibrates the strength of mathematical theorems against subsystems of second-order arithmetic — RCA₀, WKL₀, ACA₀, ATR₀, Π¹₁-CA₀ — all extending Peano-style first-order arithmetic.
• Recursion theorem. The proof that primitive recursive definitions actually define functions ultimately uses induction. Every recursive program a CS undergraduate writes is a Peano-style induction in disguise.
• Categoricity vs. completeness. Second-order PA is categorical (one model) but incomplete (some second-order truths unprovable due to Henkin semantics issues). First-order PA is complete in another sense (axiomatized by a recursive set) but incomplete in Gödel's sense (some truths unprovable). The contrast clarifies subtle features of formal systems.
• Bridge to Gödel. Peano arithmetic is the simplest theory strong enough to prove the incompleteness theorems. Studying PA is the natural entry point for studying the limits of formal systems.

The five modern axioms

Let ℕ denote the set we are characterizing, with a designated element 0 ∈ ℕ and a function S : ℕ → ℕ.

1. 0 is a natural number. 0 ∈ ℕ.
2. Every natural number has a successor. For all n ∈ ℕ, S(n) ∈ ℕ.
3. 0 is not a successor. For all n ∈ ℕ, S(n) ≠ 0.
4. The successor function is injective. If S(m) = S(n) then m = n.
5. Mathematical induction. If A is a subset of ℕ such that 0 ∈ A and for every n ∈ A we also have S(n) ∈ A, then A = ℕ.

The first four axioms alone fail to determine ℕ: a model could include extra ghost elements that are not reachable from 0 by finitely many applications of S. The induction axiom rules out such phantoms — it forces every element of ℕ to be reachable from 0 in finitely many successor steps.

Peano's original 1889 paper used nine axioms; the redundancies were stripped away over the years. The modern five-axiom statement is essentially due to Dedekind (whose 1888 essay Was sind und was sollen die Zahlen? appeared a year before Peano), with Peano's clean symbolic notation that became standard.

Recursive definitions

From 0 and S we build all of arithmetic by primitive recursion. Addition:

• a + 0 = a (base case)
• a + S(b) = S(a + b) (recursive step)

Multiplication:

• a × 0 = 0
• a × S(b) = a + (a × b)

Exponentiation:

• a^0 = 1
• a^S(b) = a × a^b

The recursion theorem of Dedekind (1888) guarantees these prescriptions actually define functions ℕ × ℕ → ℕ. Without induction, the recursion theorem fails — nonstandard models would have multiple "extensions" of partial recursive definitions.

First-order Peano arithmetic (PA)

PA is the first-order theory in the language {0, S, +, ×, =} (and order ≤ as derived). The axioms are: the four non-induction axioms above expressed in first-order logic, the recursive definitions of + and × as axioms, and the first-order induction schema — for each formula φ(x, ȳ), the axiom

(φ(0, ȳ) ∧ ∀n (φ(n, ȳ) → φ(S(n), ȳ))) → ∀n φ(n, ȳ).

This schema has infinitely many instances, one per formula. The compactness theorem of first-order logic guarantees PA admits nonstandard models — in fact, models of every cardinality ≥ ℵ₀.

Incompleteness

Gödel's first incompleteness theorem (1931) shows PA is incomplete: there is a sentence G in the language of PA such that PA proves neither G nor ¬G, assuming PA is consistent. The sentence G is constructed via Gödel numbering — encoding formulas as natural numbers — and the diagonal lemma, which produces a sentence that effectively says "I am not provable in PA." The proof is constructive: G can be written down explicitly given a description of PA's axioms.

The second incompleteness theorem (1931) strengthens this dramatically. The arithmetic statement Con(PA) — formalizing "PA does not prove a contradiction" — is itself unprovable in PA, assuming PA is consistent. So PA cannot bootstrap a proof of its own consistency. Gentzen (1936) gave a consistency proof using transfinite induction up to ε₀, sidestepping the incompleteness barrier by using a stronger meta-theory.

Second-order PA and categoricity

Second-order PA replaces the first-order induction schema with the single second-order axiom: for every subset A of ℕ, if 0 ∈ A and S(n) ∈ A whenever n ∈ A, then A = ℕ. Quantification ranges over all subsets, not just definable ones. With full second-order semantics, second-order PA is categorical — every model is isomorphic to the standard ℕ.

The catch: full second-order semantics is itself not first-order axiomatizable. With the weaker Henkin semantics (where second-order quantifiers range only over a designated collection of subsets), nonstandard models reappear. Categoricity is a feature of the intended semantics, not a property that survives translation into first-order logic.

Von Neumann's construction in ZF

Within ZF, the natural numbers are constructed concretely. Define 0 = ∅, and for any set n let S(n) = n ∪ {n}. Then 1 = {∅}, 2 = {∅, {∅}}, 3 = {∅, {∅}, {∅, {∅}}}, and in general n = {0, 1, ..., n-1}. The axiom of infinity asserts there is a set I with ∅ ∈ I and (x ∈ I ⇒ S(x) ∈ I). The intersection of all such inductive sets is ℕ — the smallest inductive set.

The Peano axioms are then provable theorems in ZF: 0 ∈ ℕ by infinity, S is injective by extensionality (m ∪ {m} = n ∪ {n} implies m = n), no n has S(n) = 0 because S(n) is nonempty, and induction is the very definition of ℕ as the smallest inductive set.

Common misconceptions

• PA describes all of ℕ. First-order PA admits nonstandard models with infinite elements. Only second-order PA with full semantics is categorical, and that requires a stronger meta-theory.
• Induction is a theorem. In PA induction is an axiom (or schema). It can be proved as a theorem in ZF using the von Neumann construction, but in pure arithmetic without set theory it must be assumed.
• Successor is +1. S is just a unary function with the listed properties. The interpretation as +1 emerges only after defining addition recursively. Different models could realize S as different operations and still satisfy axioms 1-4.
• Peano axioms imply ℕ is unique. They imply uniqueness only in second-order logic with full semantics. Skolem (1934) showed that any first-order theory with an infinite model has nonstandard models — a fundamental limitation of first-order arithmetic.
• 0 should be 1. Peano started with 1 in 1889, then later switched to 0. Modern logic and computer science prefer 0 because it makes additive identities clean and matches array indexing conventions.
• Gödel proved PA is wrong. Gödel proved PA is incomplete — there are true statements about ℕ that PA cannot prove. PA itself is not wrong; it is consistent (assuming arithmetic is consistent), just not strong enough to prove every truth.

Legacy and modern role

The Peano axioms remain the standard formal foundation for arithmetic in 2026. They appear at the start of every undergraduate logic textbook, in the kernels of every major proof assistant (Coq, Lean, Isabelle, Agda), and in the type-theoretic foundations of dependently typed programming languages. Reverse mathematics quantifies the proof-theoretic strength of theorems against subsystems of arithmetic that look unmistakably Peano-shaped. After 137 years, Peano's framework still carries the load.