Talks

Slides from public lectures that I have given.

• Unwinding Furstenberg's proof of Szemerédi's theorem
  Slides: pdf
   
• Computability and 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 a paper of the same name
  Abstract: html. Slides: pdf
   
• A formally verified proof of the prime number theorem
  Based on a paper of the same name
  Slides: pdf
   
• Translating nonstandard proofs to constructive ones
  Uses a nonstandard proof by Renling Jin to find an elementary proof of Steinhaus' theorem
  Notes: html. Slides: pdf
   
• Proof mining
  A three-lecture tutorial
  Abstract: pdf. 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
  Slides: dvi, postscript, pdf
   
• Update procedures and the 1-consistency of arithmetic
  An overview of the paper with the same name
  Slides: dvi, postscript, pdf
   
• Eliminating definitions and Skolem functions in first-order logic
  An overview of the paper with the same name
  Slides: dvi, postscript, pdf, postscript 2up, pdf 2up
   
• Semantic approaches to ordinal analysis
  Primarily an overview of "An ordinal analysis of admissible set theory using recursion on ordinal notations"
  Slides: dvi, postscript, pdf, postscript 2up, pdf 2up
   
• Weak theories of nonstandard arithmetic and analysis
  An overview of the paper with the same name
  Abstract: html. Slides: dvi, postscript, pdf, postscript 2up, pdf 2up
   
• Between proof theory and model theory
  An overview of "Saturated models of universal theories"
  Abstract: html. Slides: dvi, postscript, pdf, postscript 2up, pdf 2up
   
• Cut elimination revisited
  An overview of "Algebraic proofs of cut elimination"
  Slides: dvi, postscript, pdf
   
• Sheaf semantics and nonstandard intuitionistic arithmetic
  An overview of "Transfer principles in nonstandard intuitionistic arithmetic," for classical logicians
  Slides: dvi, postscript, pdf
   
• Semantic methods in proof theory
  A survey
  Slides: dvi, postscript, pdf
   
• Interpreting classical theories in constructive ones
  An overview of the paper with the same name
  Slides: dvi, postscript, pdf
   
• A realizability interpretation for classical arithmetic
  An overview of the paper with the same name
  Slides: dvi, postscript, pdf
   
• The combinatorics of propositional provability
  An overview of "Plausibly hard combinatorial tautologies"
  Slides: dvi, postscript, pdf
   
• Proof theory and subsystems of second-order arithmetic
  A survey of some of my work in proof theory
  Slides: dvi, postscript, pdf