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):

∀x. S(x) ≠ 0
∀x,y. S(x) = S(y) → x = y
∀x. x + 0 = x
∀x,y. x + S(y) = S(x + y)
∀x. x × 0 = 0
∀x,y. x × S(y) = (x × y) + x
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.

Symbol	Unicode	Name	Meaning
0	—	Zero	First natural number
S	—	Successor	Next number
+	—	Plus	Addition
×	—	Times	Multiplication
ℕ	U+2115	Naturals	Standard model
ω	U+03C9	Omega	Order type of ℕ
ε₀	—	Epsilon-zero	Ordinal for PA
Con	—	Consistency	Consistency statement

Metatheory. PA is incomplete: Gödel sentences true but unprovable. ω-consistent: can't prove n is not a proof for each n, then prove ∃n.Proves(n). Non-standard models have infinite numbers. PA proves ∀n.φ(n) only if provably total. Proof-theoretic ordinal of PA is ε₀. Cuts in PA correspond to truth predicates.

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. Incomplete: some true statements unprovable. Non-standard models complicate semantics. No first-order truth definition (Tarski). Higher-order needed for full completeness. Induction schema infinitely many axioms. Computational complexity of proof search high.