Proof Theory and Proof Mining

Table of Contents

Below are the slides from a series of five one-hour lectures that I presented to the Summer School in Logic in Helsinki in 2015, together with outlines and suggested reading.

I did not get to the fourth topic, but the slides I would have used are included.

1 Computable analysis

Slides: Part I


  • computable functions and the halting problem
  • computable reals and Specker sequences
  • computable functions on the real numbers
  • moduli of continuity, compactness, and the low basis theorem
  • computable metric spaces
  • computable structures (Hilbert spaces, Banach spaces, measure spaces)
  • computability and convergence theorems
  • computability in ergodic theory
  • primitive recursive functions and functionals

Suggested Reading:

2 Formal theories of analysis

Slides: Part II


  • primitive recurive arithmetic
  • first-order arithmetic
  • the double-negation interpretation
  • second-order arithmetic
  • subsystems of second-order arithmetic
  • RCA0, and conservation over ISigma1
  • WKL0, and conservation over RCA0
  • ACA0, and conservation over PA
  • formalizing analysis
  • theories of finite type, PRAomega, etc.
  • conservativity of "all sets Lebesgue measurable" over ACA0

Suggested Reading:

3 The Dialectica interpretation and applications

Slides: Part III


  • The Dialectica interpretation
  • benefits of the interpretation
  • the monotone Dialectica interpretation
  • a metatheorem by Kohlenbach
  • applications
  • convergence theorems revisted
  • metastability
  • oscillations

Suggested Reading:

4 Ultraproducts and nonstandard analysis

Slides: Part IV


  • nonstandard analysis
  • weak theories of nonstandard analysis
  • conservation result for ultraproducts
  • ultraproducts and metastability

Suggested Reading:

5 Additional slides

Slides: extra slides

These are extra slides I used before each lecture other than the first, mainly to recap the material from the previous lecture.

6 What's left out

To maintain focus, I had to avoid a number of topics that are interesting, important, and integrally connected with the ones listed above. These include:

  • reverse mathematics of stronger theories (ATR0, Pi11-CA0, …)
  • constructive mathematics and constructive analysis
  • reverse mathematics and combinatorics
  • proof mining and combinatorics
  • ultraproducts and nonstandard methods in combinatorics

Author: Jeremy Avigad

Created: 2015-07-30 Thu 15:36

Emacs 24.4.1 (Org mode 8.2.10)