11.3 Reverse mathematics and proof-theoretic strength

Reverse mathematics explores the axioms needed to prove theorems in mathematics. It's like figuring out the minimum ingredients for a recipe. This approach helps us understand the foundations of math and how different parts connect.

The big five subsystems of second-order arithmetic are key players in this field. They range from the basic $RCA_0$ to the powerful $\Pi^1_1-CA_0$, each with its own strengths and capabilities in proving theorems.

Reverse Mathematics and Subsystems

Overview of Reverse Mathematics

• Reverse mathematics studies the strength of axioms needed to prove theorems
• Involves proving equivalences between theorems and axioms over a weak base theory
• Base theory is typically a subsystem of second-order arithmetic
• Goal is to determine the minimal axioms required for proving specific theorems

Subsystems of Second-Order Arithmetic

• Second-order arithmetic extends first-order Peano arithmetic with sets and quantification over sets
• Subsystems are formed by restricting the comprehension axiom schema
• Common subsystems include $RCA_0$, $WKL_0$, $ACA_0$, $ATR_0$, and $\Pi^1_1-CA_0$
• Subsystems are linearly ordered by inclusion and consistency strength

The Big Five Subsystems

• The big five are the most commonly studied subsystems in reverse mathematics
• $RCA_0$ (Recursive Comprehension Axiom): Includes comprehension for computable sets and $\Sigma^0_1$-induction
• $WKL_0$ (Weak König's Lemma): Extends $RCA_0$ with a compactness principle for infinite binary trees
• $ACA_0$ (Arithmetical Comprehension Axiom): Allows comprehension for arithmetically definable sets
• $ATR_0$ (Arithmetical Transfinite Recursion): Extends $ACA_0$ with transfinite recursion of arithmetic predicates
• $\Pi^1_1-CA_0$ ($\Pi^1_1$-Comprehension Axiom): Allows comprehension for $\Pi^1_1$ formulas

Proof-Theoretic Strength

• Proof-theoretic strength measures the strength of a theory in terms of the functions it can prove total
• Commonly measured using ordinal notations and fast-growing hierarchies
• The big five have well-understood proof-theoretic strengths:
  • $RCA_0$ and $WKL_0$: Prove the totality of primitive recursive functions
  • $ACA_0$: Proves the totality of $\epsilon_0$-recursive functions (Ackermann-level)
  • $ATR_0$: Proves the totality of $\Gamma_0$-recursive functions (non-primitive recursive)
  • $\Pi^1_1-CA_0$: Has the strength of finitary Zermelo-Fraenkel set theory

Comprehension and Induction

Comprehension Axioms

• Comprehension axioms assert the existence of sets defined by formulas
• General form: $\exists X \forall n (n \in X \leftrightarrow \varphi(n))$ for a formula $\varphi$
• Unrestricted comprehension leads to inconsistency (Russell's paradox)
• Subsystems of second-order arithmetic restrict comprehension to specific formula classes

Induction Principles

• Induction principles allow proving statements for all natural numbers
• First-order induction: $(\varphi(0) \land \forall n (\varphi(n) \rightarrow \varphi(n+1))) \rightarrow \forall n \varphi(n)$
• Second-order arithmetic includes induction for formulas with set quantifiers
• Restricted induction schemes are often used, such as $\Sigma^0_1$-induction in $RCA_0$

Arithmetical Comprehension

• Arithmetical comprehension allows forming sets defined by arithmetic formulas
• Arithmetic formulas are those with only number quantifiers (no set quantifiers)
• The system $ACA_0$ includes arithmetical comprehension
• Equivalent to the existence of the Turing jump of any set

$\Pi^1_1$-Comprehension

• $\Pi^1_1$-comprehension allows forming sets defined by $\Pi^1_1$ formulas
• $\Pi^1_1$ formulas have a universal set quantifier followed by an arithmetic formula
• The system $\Pi^1_1-CA_0$ includes $\Pi^1_1$-comprehension
• Equivalent to the existence of a Suslin set (a specific $\Pi^1_1$ set)

Key Principles

Weak König's Lemma (WKL)

• Weak König's Lemma is a compactness principle for infinite binary trees
• States that every infinite binary tree has an infinite path
• Equivalent to the compactness of propositional logic over $RCA_0$
• Strictly stronger than $RCA_0$ but weaker than $ACA_0$
• Used to prove the completeness theorem and the Heine-Borel covering lemma

Reverse Mathematics of WKL

• Many theorems in analysis and algebra are equivalent to $WKL_0$ over $RCA_0$
• Examples include the intermediate value theorem and the existence of algebraic closures
• These equivalences show that WKL is necessary and sufficient for proving these theorems
• Demonstrates the role of compactness in many areas of mathematics

Applications and Consequences

• Reverse mathematics has been applied to many areas, including analysis, algebra, and combinatorics
• Has revealed the role of set existence principles and induction in ordinary mathematics
• Provides a fine-grained analysis of the strength of mathematical theorems
• Connections with computability theory, descriptive set theory, and constructivism