Advanced course at the 34th European Summer School in Logic, Language and Information.
Lectured by Anupam Das.
Proof theory is one of the “four pillars” of mathematical logic, and is of fundamental interest to mathematicians, computer scientists, philosophers and linguists alike. It serves as the foundation for many other endeavours in logic and has also been useful in realising the interplay between logic and other areas of mathematics, not least via the theory of computation.
This course will introduce students to the fundamentals of the proof theory of arithmetic. We shall assume some previous familiarity with basic proof theory, but will go further to show how to apply these techniques in order to obtain metalogical results of profound importance at the interface between logic and computation. Namely, we shall present a seminal consistency proof of Peano Arithmetic (PA) via infinitary cut-elimination, and following on from that derive a famous classification of PA’s provably total recursive functions. We will also survey other consistency proofs and computational interpretations, discuss the adaptation of these results to important fragments and extensions of PA.
Outline of the course
The lectures will provisionally be structured as follows (to be updated during the week):
- Lecture 1 (Monday). The rise of proof theory. Background on proof theory, the foundational crisis, Hilbert’s program, Goedel’s incompleteness theorems, Gentzen’s cut-elimination theorem.
[slides, updated 08-08-23]
Accessibility: This is a mostly non-technical lecture. It should be accessible to all ESSLLI participants. - Lecture 2 (Tuesday). Peano Arithmetic. Syntax and semantics of first-order arithmetic, examples of inductive reasoning, sequent calculus.
[slides, updated 17-08-23] [annotated slides]
Accessibility: This is a preliminary lecture. It should be accessible to most ESSLLI participants. - Lecture 3 (Wednesday). Two consistency proofs. Soundness (formalised), an infinitary system, cut-elimination, ordinal bounds.
[slides, updated 17-08-23] [annotated slides]
Accessibility: This is a technical lecture building on Lecture 2. It should be accessible to ESSLLI participants with some background in proof theory. - Lecture 4 (Thursday). Provably recursive functions. Ordinal notations, transfinite recursion, examples of higher recursion, Kleene realisability (time permitting).
[slides] [annotated slides]
Accessibility: This is a technical lecture building on Lecture 2 (but mostly independent of Lecture 3). It should be accessible to ESSLLI participants with some background in proof theory. - Lecture 5 (Friday). Further directions. Fragments of PA, extensions of PA, second-order arithmetic.
[slides] [annotated slides]
Accessibility: This is a survey style lecture. It should be accessible to most ESSLLI participants.
Recommended reading
There are many excellent textbooks on the proof theory of arithmetic that have influenced this course, including but not limited to:
- Proof Theory. Gaisi Takeuti. 1975
- Proof Theory: an Introduction. Wolfram Pohlers. 1989.
- Handbook of Proof Theory. Sam Buss (editor). 1998.
- Basic Proof Theory. Anne Troelstra and Helmut Schwichtenberg. 1996.
- Ordinal Analysis with an Introduction to Proof Theory. Toshiyasu Arai. 2020.
Naturally, for an intensive one-week course, it is impossible to present all material at the finest level of detail. The references above should be consulted for more low-level details on the definitions and results given in the course. Specific references will be made clear in each lecture.
In addition, the Stanford Encyclopedia of Philosophy is an excellent source of introductory articles on a range of subjects in proof theory, including Proof Theory, Hilbert’s Program, Gödel’s Incompleteness Theorems, and many more.