Proof Interpretations: a modern perspective

Course at NASSLLI ’18: Logic and Computation theme. Baker Hall 235B, Carnegie Mellon University.
Lectured by Anupam Das and Thomas Powell.

This page will contain resources and useful information for the course once they are available.

Motivation and description

In the 1930s, in the midst of 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. 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, System T, 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 up to the point where some of their many and varied roles in modern research can be understood and appreciated. We will assume a basic familiarity with the proof theory of first-order logic, but intend to frame the course so that it is accessible and interesting for mathematicians, philosophers, linguists and computer scientists alike.