# Proof theory of arithmetic

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.