Reverse Mathematics

Origin. Friedman initiated reverse mathematics (1970s). Simpson systematized (1999). Studies which axioms are needed to prove theorems. Five main subsystems of second-order arithmetic. Calibrates logical strength of ordinary mathematics.

Models. Axioms required for theorems. Forward: axioms → theorems. Reverse: theorem → which axioms needed? Most theorems equivalent to one of "Big Five" systems. Classifies mathematical content by logical strength.

Formalism.

Base system RCA₀: Recursive Comprehension Axiom. Δ⁰₁ comprehension, Σ⁰₁ induction — superscript 0 for arithmetical (no set quantifiers), subscript 1 for one alternation. The other Big Five systems are indexed the same way, which is why Π¹₁-CA₀ carries a superscript 1: it quantifies over sets. Δ⁰₁ comprehension is not "comprehension for recursive φ" — Δ⁰₁ is not a syntactic class, so the axiom must be stated with a hypothesis: if φ is Σ⁰₁ and ψ is Π⁰₁ and ∀n (φ(n) ↔ ψ(n)), then {n : φ(n)} exists. Encodes computable mathematics.

The Big Five:

RCA₀: computable mathematics
WKL₀: weak König's lemma (binary tree)
ACA₀: arithmetical comprehension
ATR₀: arithmetical transfinite recursion
Π¹₁-CA₀: Π¹₁ comprehension

Hierarchy: RCA₀ < WKL₀ < ACA₀ < ATR₀ < Π¹₁-CA₀

Equivalences:

Bolzano-Weierstrass ↔ ACA₀
Ramsey's theorem for pairs ↔ between RCA₀ and ACA₀
Completeness of FOL ↔ WKL₀
Countable basis theorem ↔ ACA₀

Methodology: Prove: RCA₀ + theorem → axiom. This shows axiom necessary for theorem. Often: theorem ↔ axiom over base.

Conservation: WKL₀ is Π¹₁-conservative over RCA₀. Some systems don't add Π¹₁ consequences.

Symbols.

Symbol	Unicode	Name	Meaning
RCA₀	—	Recursive comp	Base system
WKL₀	—	Weak König	Binary tree lemma
ACA₀	—	Arithmetical comp	Full arithmetic comprehension
ATR₀	—	Arith transfinite	Transfinite recursion
Π¹₁-CA₀	—	Pi-1-1 comp	Π¹₁ comprehension
↔	U+2194	Equivalent	Over base
→	U+2192	Implication	Direction of a reversal
Z₂	—	Second-order arithmetic	The full system the five are fragments of
Δ⁰₁, Σ⁰₁, Π¹₁	—	Arithmetical and analytical classes	Comprehension and induction parameters
ε₀	—	Epsilon-nought	Proof-theoretic ordinal of ACA₀
Γ₀	—	Feferman–Schütte ordinal	Ordinal of ATR₀; the limit of predicativity
RT²₂	—	Ramsey for pairs	The standard exception to the Big Five

Metatheory. Every reversal is proved over RCA₀, which must be weak enough for the reversal to be informative and strong enough to carry the coding of analysis. The calibrations are exact equivalences: Heine–Borel compactness of [0,1], the Gödel completeness theorem, Brouwer's fixed-point theorem and Peano's existence theorem for ordinary differential equations are each equivalent to WKL₀; Bolzano–Weierstrass, Ascoli's theorem, and Ramsey's theorem for triples to ACA₀; comparability of countable well-orderings and open determinacy to ATR₀ (Steel); the Cantor–Bendixson theorem to Π¹₁-CA₀. Conservation gives the systems proof-theoretic content — WKL₀ is Π⁰₂-conservative over primitive recursive arithmetic, Simpson's partial realization of Hilbert's programme, and Π¹₁-conservative over RCA₀ (Harrington); ACA₀ is conservative over PA for arithmetical sentences. Proof-theoretic ordinals separate the levels: ω^ω for RCA₀ and WKL₀, ε₀ for ACA₀, Γ₀ for ATR₀, the Feferman–Schütte bound on predicativity. Ramsey's theorem for pairs is the standard exception, shown not to imply ACA₀ (Seetapun and Slaman, 1995) and not to imply WKL₀ (Liu, 2012).

Applies to. Foundations of mathematics. Calibrating mathematical content. Computability connections. Proof theory. Mathematical logic. Philosophy of mathematics.

Limitations. Everything must be coded as a countable object: a real is a Cauchy sequence with a modulus, a continuous function is a code for its values on rationals, a separable space is a countable dense subset. Statements about arbitrary uncountable structures are not expressible at all, and placements are sensitive to the coding, so what is measured is the strength of a formalization rather than of a theorem simpliciter. The Big Five is an empirical regularity with no proof and with known exceptions: Ramsey's theorem for pairs sits strictly between RCA₀ and ACA₀ and matches neither, and the principles below it — COH, ADS, CAC, stable Ramsey — form a partial order with many incomparable nodes. The base system is itself a commitment, since RCA₀ carries Σ⁰₁ induction and is therefore not neutral. And nothing on this scale reaches the strength of set-theoretic principles about uncountable cardinals.