# Proof Theory and Proof Mining

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

Topics:

• 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

Topics:

• 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

Topics:

• 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

Topics:

• 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

Created: 2015-07-30 Thu 15:36

Emacs 24.4.1 (Org mode 8.2.10)

Validate