Peano Arithmetic (PA)

Origin. Peano formalized arithmetic axioms (1889). Gödel proved incompleteness (1931): PA cannot prove its own consistency. Gentzen proved PA consistent using transfinite induction (1936). Foundation of metamathematics and proof theory. Various subsystems studied in reverse mathematics.

Models. Natural numbers and their properties. Peano Arithmetic (PA) axiomatizes ℕ with successor, addition, multiplication. Intended model: standard natural numbers. Non-standard models exist: have "infinite" numbers satisfying all PA axioms. Incompleteness: PA true statements not provable in PA.

Formalism.

Language:

• Constants: 0
• Functions: S (successor), +, ×
• Relation: = (equality)

Peano Axioms (PA):

1. ∀x. S(x) ≠ 0
2. ∀x,y. S(x) = S(y) → x = y
3. ∀x. x + 0 = x
4. ∀x,y. x + S(y) = S(x + y)
5. ∀x. x × 0 = 0
6. ∀x,y. x × S(y) = (x × y) + x
7. Induction: φ(0) ∧ ∀x.(φ(x) → φ(S(x))) → ∀x.φ(x) (for each formula φ)

Subsystems:

• PRA (Primitive Recursive Arithmetic): quantifier-free, functions defined by primitive recursion
• IΣ₁: induction restricted to Σ₁ formulas
• PA⁻: PA without induction scheme
• Second-order arithmetic (Z₂): quantify over sets

Key theorems:

• Gödel's First: PA incomplete if consistent
• Gödel's Second: PA cannot prove Con(PA)
• Gentzen: ε₀-induction proves Con(PA)

Reverse mathematics hierarchy: RCA₀ < WKL₀ < ACA₀ < ATR₀ < Π¹₁-CA₀

Symbols.

Metatheory. Gödel (1931) proved PA incomplete: if PA is ω-consistent there is a Π⁰₁ sentence it neither proves nor refutes, and Rosser (1936) replaced ω-consistency by plain consistency. The second theorem — PA ⊬ Con(PA) if PA is consistent — needs the Hilbert–Bernays–Löb derivability conditions on the provability predicate, and fails for provability predicates that violate them. Gentzen (1936) proved Con(PA) from primitive recursive arithmetic plus quantifier-free transfinite induction up to ε₀, which is exact: PA proves transfinite induction for every α < ε₀ and not for ε₀, so ε₀ is PA's proof-theoretic ordinal, and PA's provably total functions are those in the fast-growing hierarchy below ε₀. PA is not finitely axiomatizable (Ryll-Nardzewski 1952) — the IΣₙ hierarchy is strict and every finite subtheory sits inside some level. It is essentially undecidable, since it interprets Robinson's Q. Semantically it is far from ℕ: compactness gives nonstandard models, every countable one has order type ω + (ω* + ω)·η, MacDowell and Specker (1961) showed every model has a proper elementary end extension, and Tennenbaum (1959) showed no nonstandard model of PA is computable. Paris and Harrington (1977) gave the first natural Π⁰₂ sentence true but unprovable in PA; Kirby and Paris (1982) did the same with Goodstein's theorem and the hydra game.

Applies to. Foundations of mathematics. Cryptography (number theory). Proof theory and ordinal analysis. Automated theorem proving. Verified arithmetic (hardware, software). Philosophy of mathematics. Reverse mathematics.

Limitations. PA is essentially incomplete: every consistent r.e. extension is incomplete too, so nothing can be added to repair it while keeping the axioms effectively given. It proves neither Con(PA) nor transfinite induction to ε₀, and therefore neither Goodstein's theorem nor the Paris–Harrington principle, nor the totality of any function outgrowing the fast-growing hierarchy below ε₀. It cannot define arithmetical truth in its own language (Tarski), so satisfaction is unavailable and the induction schema reaches only formulas already in the signature — a property specified by a truth predicate falls outside it. It does not determine its subject matter: first-order induction is not categorical, Löwenheim–Skolem gives models of every infinite cardinality, and Tennenbaum's theorem means none of the countable nonstandard ones can be presented computably, so the unintended models cannot be exhibited or excluded. Second-order induction restores categoricity only by abandoning effective axiomatization.

© 2026 Lingenic LLC