Second-Order Arithmetic (Z₂)

Origin. Hilbert and Bernays formalized analysis in a two-sorted arithmetic (Grundlagen der Mathematik II, 1939). Its subsystems were mapped by Friedman (1970s) and systematized by Simpson (Subsystems of Second Order Arithmetic, 1999). Z₂ is the setting in which reverse mathematics is conducted, and the reason that programme has a fixed scale to measure against.

Models. Two sorts: numbers and sets of numbers. Enough to formalize essentially all of classical analysis and countable algebra, and little enough that its fragments can be told apart. The interest is not in Z₂ itself but in its subsystems: what you must assume to prove a given theorem of ordinary mathematics.

Formalism.

Language: Number variables m, n, ...; set variables X, Y, ... 0, S, +, ×, <, ∈ Formulas: first-order plus quantification over sets.

Basic axioms: Peano axioms without induction as a schema. Induction axiom: (0 ∈ X ∧ ∀n(n ∈ X → n+1 ∈ X)) → ∀n(n ∈ X) Comprehension: ∃X ∀n (n ∈ X ↔ φ(n)), for φ in a specified class.

The five subsystems (the Big Five): RCA₀ Δ⁰₁ comprehension + Σ⁰₁ induction — computable mathematics WKL₀ RCA₀ + weak König's lemma (every infinite binary tree has a path) ACA₀ arithmetical comprehension — equivalent to PA in first-order strength ATR₀ arithmetical transfinite recursion Π¹₁-CA₀ Π¹₁ comprehension

Full Z₂: Comprehension for all second-order formulas. Impredicative.

Strength: RCA₀ < WKL₀ < ACA₀ < ATR₀ < Π¹₁-CA₀ < Z₂ The first two agree on first-order consequences (Harrington); the jump to ACA₀ is real.

Symbols.

Metatheory. The Big Five phenomenon is the subject's central unexplained fact: theorems of ordinary mathematics almost always turn out equivalent, over RCA₀, to one of five systems, and the equivalences are proved by deriving the axiom back from the theorem — which is what makes the programme reverse. WKL₀ is Π⁰₂-conservative over primitive recursive arithmetic (Friedman), which gives Hilbert's programme a partial realization: a large slice of analysis is finitistically reducible. ACA₀ is conservative over PA. Z₂ interprets, and is interpreted in, fragments of set theory, which is how the two foundational scales are calibrated against each other.

Applies to. Reverse mathematics. Proof-theoretic strength. Predicativity and its limits (ATR₀ and Γ₀). Constructive and computable analysis, where RCA₀ is the natural base. Calibrating theorems of analysis, algebra, and combinatorics against a fixed scale.

Limitations. Only countable mathematics is directly formalizable; uncountable structures must be coded, and the coding is not neutral — a theorem's placement can depend on how its objects were represented. The Big Five is an empirical regularity with well-known exceptions, and the exceptions cluster in combinatorics (Ramsey's theorem for pairs is the standard one). Full Z₂ is impredicative and rarely the object of study; the interest is entirely in the fragments.

© 2026 Lingenic LLC