Computability Theory

Induction and conservation

The hierarchy of induction and collection schemes, the pigeonhole principle and Σ⁰₂ collection, and the conservation theorems of Friedman and Harrington.

Advanced4 lessons≈ 155 min12 questions
Progress0/12 questions answered
StartProgress is saved in this browser.

Reverse mathematics in non-standard models. The course sets up the schemes of Σ⁰ₙ induction, collection and least numbers and the Paris–Kirby hierarchy between them, proves Hirst's theorem that the infinite pigeonhole principle for arbitrarily many colors is Σ⁰₂ collection, identifies the first-order parts of RCA₀ and ACA₀, with the Jockusch–Solovay bound, and proves Harrington's theorem that weak König's lemma is Π¹₁-conservative over RCA₀ by forcing with infinite subtrees.

Contents

  1. 1

    Induction, collection and least numbers

    The schemes of Σ⁰ₙ and Π⁰ₙ induction, collection and least number principles; closure of the classes Σ⁰ₙ under bounded quantification in the presence of collection; Σ⁰ₙ and Π⁰ₙ induction are equivalent; the hierarchy IΣ⁰ₙ₊₁ ⇒ BΣ⁰ₙ₊₁ ⇒ IΣ⁰ₙ.

    1. 1.1 The schemes
    2. 1.2 Σ⁰ₙ and Π⁰ₙ induction
    3. 1.3 Induction implies collection
    4. 1.4 Least number principles
    5. 1.5 Collection implies induction
    6. 1.6 Exercises
    7. 1.7 Notes and references
    40 min
  2. 2

    The pigeonhole principle and Σ⁰₂ collection

    The infinite pigeonhole principle for arbitrarily many colors is equivalent to Σ⁰₂ collection over RCA₀ (Hirst); Ramsey's theorem for pairs implies it; first-order consequences of combinatorial principles.

    1. 2.1 Hirst's theorem
    2. 2.2 Ramsey's theorem for pairs
    3. 2.3 Exercises
    4. 2.4 Notes and references
    30 min
  3. 3

    First-order parts and conservation

    Conservative extensions and ω-extensions; ACA₀ is conservative over Peano arithmetic and RCA₀ over IΣ₁ (Friedman), by expanding a model of arithmetic with its definable sets; the Jockusch–Solovay bound on the solutions provided by ACA₀, and the unprovability of ACA₀′.

    1. 3.1 Conservative extensions
    2. 3.2 Peano arithmetic and ACA₀
    3. 3.3 IΣ₁ and RCA₀
    4. 3.4 The Jockusch–Solovay bound
    5. 3.5 Exercises
    6. 3.6 Notes and references
    40 min
  4. 4

    Harrington's conservation theorem

    WKL₀ proves the same Π¹₁ sentences as RCA₀; a forcing construction over a countable non-standard model adds a path through an infinite tree while preserving Σ⁰₁ induction; consequences for the first-order part of WKL₀.

    1. 4.1 Π¹₁ conservation
    2. 4.2 Setting
    3. 4.3 Forcing with infinite subtrees
    4. 4.4 The generic path
    5. 4.5 Consequences
    6. 4.6 Exercises
    7. 4.7 Notes and references
    45 min