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.
About the instructors
Dr. Anupam Das is a Marie Skłodowska-Curie research fellow at the University of Copenhagen. His research focusses on proof theory, the area of mathematical logic concerned with formal proofs. In particular, he is interested in the interactions between logic and computational complexity.
Dr. Thomas Powell is a postdoctoral researcher in mathematics at the Technical University of Darmstadt. His research is in mathematical logic and proof theory, with a focus on functional interpretations, the extraction of computational content from proof, and higher type computability theory.