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

Metatheory. Big Five robust: most theorems fall into them. Proof-theoretic ordinals calibrate strength. Independence: some theorems incomparable. Conservation results: relative consistency. Connections to computability theory.

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

Limitations. Second-order arithmetic context. Some theorems escape Big Five. Technical machinery required. Specialized area. Limited direct applications. Not all mathematics covered.