Thomas Powell (University of Bath)
Thomas Powell
In the early 1920s, as a response to the foundational crisis of mathematics, David Hilbert introduced his metamathematical program, aiming to reduce mathematics to a formal axiomatic system whose consistency could be proven using ‘finitary’ methods. A decade later, Gödel’s incompleteness theorems famously confirmed that Hilbert’s program, in its strictest sense, is impossible to achieve. Less recognized are Gödel’s attempts to overcome his own obstacle and tackle Hilbert’s program in broader terms. Over the following decades, Gödel developed his Dialectica interpretation, which reduced Peano arithmetic to a quantifier-free system of higher order functionals, SystemT, allowing the consistency of arithmetic to follow from that of T.
During the 1950s, Kreisel observed that proof interpretations like Gödel’s could also be viewed from another angle: as tools for extracting concrete witnesses from existential statements. In the following years these insights were developed further, and from the 1990s onwards the formal extraction of programs from proofs truly took off thanks to the ‘proof mining’ program led by Kohlenbach. As a result of this fascinating re-orientation of proof theory, there has been a resurgence of interest in proof interpretations in the last 20-30 years, inspiring research from a range of different perspectives.
The aim of this course is to provide an introduction to proof interpretations and proof mining, up to the point where some research highlights from the last decade can be understood and appreciated. I will assume a basic familiarity with first-order logic, but intend to frame the course so that it is accessible and interesting for mathematicians, philosophers and computer scientists alike.