# 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

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:

- Avigad and Brattka, "Computability and analysis: the legacy of Alan Turing"
- Computability and Complexity in Analysis
- Bishop and Bridges,
*Constructive Analysis* - Pour-el and Richards,
*Computability in Analysis and Physics* - Weihrauch,
*Computable Analysis* - Brattka, Hertling, and Weihrauch, "A tutorial on computable analysis"
- Hoyrup and Rojas, "Computability of probability measures and Martin-Löf randomness over metric spaces"

## 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
- RCA
_{0}, and conservation over ISigma_{1} - WKL
_{0}, and conservation over RCA_{0} - ACA
_{0}, and conservation over PA - formalizing analysis
- theories of finite type, PRA
^{omega}, etc. - conservativity of "all sets Lebesgue measurable" over ACA
_{0}

Suggested Reading:

- Simpson,
*Subsystems of second-order arithmetic* - Bishop and Bridges,
*Constructive Analysis* - Troelstra and van Dalen,
*Constructivism in Mathematics* - Feferman, "How a little bit goes a long way: predicative foundations of analysis"
- Avigad, "Number theory and elementary arithmetic"
- Avigad and Simic, "Fundamental notions of analysis in subsystems of second-order arithmetic"
- Kohlenbach,
*Proof Interpretations and their use in Mathematics* - Kreuzer, "Measure theory and higher order arithmetic"

## 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:

- Avigad and Feferman, "Gödel's functional ('Dialectica') interpretation"
- Kohlenbach,
*Applied Proof Theory: Proof Interpretations and their Use in Mathematics* - Kohlenbach and Oliva, "Proof mining: a systematic way of analysing proofs in mathematics"
- Towsner, "A worked example of the functional interpretation"
- Avigad, Proof mining
- Tao, Soft analysis, hard analysis, and the finite convergence principle
- Avigad and Rute, "Oscillation and the mean ergodic theorem for uniformly convex Banach spaces"

## 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:

- Goldblatt,
*Lectures on the Hyperreals: An Introduction to Nonstandard Analysis* - Keisler, Kaufman, Henson, "The strength of nonstandard methods in arithmetic"
- Keisler, Henson, "On the strength of nonstandard analysis"
- Avigad, "Weak theories of nonstandard arithmetic and analysis"
- Tanaka, "Non-standard analysis in WKL
_{0}" - Keisler, "Nonstandard Arithmetic and Reverse Mathematics"
- van den Berg, Briseid, and Safarik, "A functional interpretation for nonstandard arithmetic"
- Towsner, "Ultrafilters in reverse mathematics"
- Kreuzer, "Non-principal ultrafilters, program extraction and higher order reverse mathematics"
- Tao, Ultraproducts as a bridge between discrete and continuous mathematics
- Tao, A cheap version of nonstandard analysis
- Tao, Walsh’s ergodic theorem, metastability, and external Cauchy convergence
- Avigad and Iovino, "Ultraproducts and Metastability"

## 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 (ATR
_{0}, Pi^{1}_{1}-CA_{0}, …) - constructive mathematics and constructive analysis
- reverse mathematics and combinatorics
- proof mining and combinatorics
- ultraproducts and nonstandard methods in combinatorics