Proof Theory and Proof Mining

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"

Slides: Part II

Topics:

• primitive recurive arithmetic
• first-order arithmetic
• the double-negation interpretation
• second-order arithmetic
• subsystems of second-order arithmetic
• RCA₀, and conservation over ISigma₁
• WKL₀, and conservation over RCA₀
• ACA₀, and conservation over PA
• formalizing analysis
• theories of finite type, PRA^omega, etc.
• conservativity of "all sets Lebesgue measurable" over ACA₀

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"

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"

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₀"
• 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"

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.

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₀, Pi¹₁-CA₀, …)
• constructive mathematics and constructive analysis
• reverse mathematics and combinatorics
• proof mining and combinatorics
• ultraproducts and nonstandard methods in combinatorics