Talks
These are slides from public lectures that I have given.
- Computability in ergodic theory
An overview. Slides: pdf.
- The computational content of classical
arithmetic
An overview of the paper with the same
title. Slides: pdf.
- Metastability in ergodic theory
A quick
overview of results in "Local stability of ergodic
averages" and "Metastability in the Furstenberg-Zimmer
tower". Slides: pdf.
- The role of the diagram in Euclid's
Elements
An overview of the paper "A
formal system for Euclid's Elements". Slides: pdf.
- Computability in ergodic theory
An
overview of the paper "Local stability of ergodic
averages". Slides: pdf.
- Verifying real inequalities
An overview of
the paper "Combining decision procedures for the reals". Slides:
pdf.
- Methodology and metaphysics in the development of
Dedekind's theory of ideals
Based on the paper with the
same title. Slides: pdf.
- A formally verified proof of the prime number
theorem
Based on a paper of the same title. Slides:
pdf.
- Translating nonstandard proofs to constructive
ones
Uses a nonstandard proof by Renling Jin to find
an elementary proof of Steinhaus' theorem. Slides: pdf. Additional
notes: html.
- Proof mining
A three-lecture tutorial.
Slides: pdf.
- Distances, projections, and the mean ergodic theorem in
subsystems of second-order arithmetic
A preliminary
presentation of some of the results in "Fundamental notions
of analysis in subsystems of second-order arithmetic".
Slides: pdf.
- Forcing in proof theory
A survey of
applications of forcing to proof theory, based on the paper of the
same title. Slides: pdf.
- Update procedures and the 1-consistency of
arithmetic
An overview of the paper with the same
title. Slides: pdf.
- Eliminating definitions and Skolem functions in
first-order logic
An overview of the paper with the
same title. Slides: pdf.
- Semantic approaches to ordinal analysis
Primarily an overview of "An ordinal analysis of admissible
set theory using recursion on ordinal notations". Slides: pdf.
- Weak theories of nonstandard arithmetic and
analysis
An overview of the paper with the same title.
Slides: pdf.
- Between proof theory and model theory
An
overview of "Saturated models of universal theories".
Slides: pdf.
- Cut elimination revisited
An overview of
"Algebraic proofs of cut elimination". Slides: pdf.
- Sheaf semantics and nonstandard intuitionistic
arithmetic
An overview of "Transfer principles
in nonstandard intuitionistic arithmetic," for classical
logicians. Slides: pdf.
- Semantic methods in proof theory
A
survey. Slides: pdf.
- Interpreting classical theories in constructive
ones
An overview of the paper with the same title.
Slides: pdf.
- A realizability interpretation for classical
arithmetic
An overview of the paper with the same
title. Slides: pdf.
- The combinatorics of propositional
provability
An overview of "Plausibly hard
combinatorial tautologies". Slides: pdf.
- Proof theory and subsystems of second-order
arithmetic
A survey of some of my work in proof
theory. Slides: pdf.