# Introduction to Proof Theory

Introductory course at Midlands Graduate School 2021.
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 world of proof theory from acomputational perspective. The overall aim is to leave the student with an appreciation of how proof theory can be exploited to obtain interesting properties of logics, and how it relates to computation. Moreover this course should suffice to prepare a student for more advanced topics in logic and proof theory.

NB: this course is based on the eponymous course from ESSLLI ’18, there co-lectured with Thomas Powell.

Outline of the course

The lectures will provisionally be structured as follows (to be updated during the week):

• Monday. First-order logic: syntax and semantics. The language of predicate logic; structures and models; a Hilbert-Frege deductive system; the deduction theorem; first-order theories and arithmetic. [slides] [some solutions to exercises]
• Tuesday. Metalogical foundations. The deduction theorem; soundness; completeness; compactness; applications. [slides] [annotated slides] [solutions to exercises]
• Wednesday. Gentzen’s sequent calculus. The problem of proof search; analyticity; rules and duality; cut-free proofs; consequences of cut-elimination. [slides] [annotated slides] [exercises] [solutions]
• Thursday. Hauptsatz: the cut-elimination theorem. Subject of structural proof theory; cut-elimination argument; non-confluence and non-termination; multiset measure; proof of Herbrand’s theorem. [slides] [annotated slides] [exercises] [some solutions to exercises]
• Friday. Perspectives: the computational content of proofs. Metamathematical consequences; scalability; computational content; normalisation for natural deduction; Curry-Howard correspondence. [whiteboard]

Exercises for each lecture can be found at the end of the corresponding slides.