Second-Order Arithmetic

Second-order arithmetic (Z₂) is a formal system that extends first-order arithmetic by allowing quantification over sets of natural numbers, in addition to quantification over individual natural numbers. It is the natural habitat of most theorems of classical analysis — results about real numbers, continuous functions, sequences, and measure — because these can be coded as statements about sets of naturals. Second-order arithmetic is weaker than full set theory but far stronger than first-order Peano Arithmetic, and its subsystems form the primary object of study in reverse mathematics.

Subsystems and the Big Five

The program of Reverse Mathematics identified five principal subsystems of second-order arithmetic, ordered by strength, that suffice to prove nearly all theorems of classical mathematics:

1. RCA₀ (Recursive Comprehension Axiom) — the base system, roughly equivalent to computable mathematics; proves facts about computable functions and computably enumerable sets.
2. WKL₀ (Weak König's Lemma) — adds the principle that any infinite binary tree has an infinite path; equivalent over RCA₀ to many compactness arguments in analysis.
3. ACA₀ (Arithmetical Comprehension Axiom) — allows comprehension for arithmetical formulas; proves the Bolzano-Weierstrass theorem and many basic theorems of analysis.
4. ATR₀ (Arithmetical Transfinite Recursion) — allows transfinite recursion along well-orders; sufficient for much of classical descriptive set theory.
5. Π¹₁-CA₀ (Π¹₁ Comprehension Axiom) — the strongest of the five; proves the existence of certain perfect kernels and related results.

The remarkable discovery of reverse mathematics is that most theorems of ordinary mathematics are equivalent to exactly one of these five systems over RCA₀. The equivalence runs in both directions: the system proves the theorem, and the theorem (over RCA₀) implies the key axiom of the system. Mathematical theorems, rather than lying on a continuum of strength, cluster at discrete levels — a structural fact about mathematics that was unknown before Harvey Friedman began the program in the 1970s.

Proof-Theoretic Ordinals of the Subsystems

Each subsystem has a corresponding proof-theoretic ordinal that measures its strength:

• RCA₀ ≡ ε₀ (same as Peano Arithmetic)
• WKL₀ ≡ ε₀ (conservative over RCA₀ for arithmetic sentences)
• ACA₀ ≡ ε₀ · ω (strictly stronger)
• ATR₀ ≡ Γ₀ (the Feferman-Schütte ordinal, limit of predicative mathematics)
• Π¹₁-CA₀ ≡ ψ(Ω_ω) (a large countable ordinal requiring impredicative methods)

The jump from ATR₀ to Π¹₁-CA₀ is the jump from predicative to impredicative mathematics — a philosophically significant boundary that second-order arithmetic makes precisely measurable.

Second-order arithmetic is the strongest reason for thinking that the foundations of analysis are tractable: nearly all of classical mathematics fits into five discrete levels, each with a precise proof-theoretic ordinal. If mathematical foundations were as murky as philosophical tradition suggests, this discrete structure would not exist.