Proof Theory

Introductory course at MGS 2022

Lecturers: Gianluca Curzi and Marianna Girlando

Proof theory studies proofs as mathematical objects, and operates at the interface between computer science, mathematics and philosophy.
Proof theoy has its historical roots in Aristotle's and Leibniz's idea of formalising and automating inferences and reasoning. In the XX century, proof theory developed into formal discipline, and became the main tool of Hilbert's program, whose goal was to prove the consistency of arithmetic through formalisation of proofs. Gödel's incompleteness theorems marked the failure of Hilbert's program, but not of proof theory, that nowadays finds relevant applications in computer science.

In this course we will introduce the main concepts and tools of proof theory. The general aim is to familiarise students with logic and formal systems, to present the main theoretical results of the discipline, and to offer an overview of the relations of proof theory with other fields, such as theory of computation. This course is intended to be introductory, and no prior knowledge on the topic is expected. The course is meant to prepare students to more advanced topics in proof theory.

Outline of the course

This course consists of 5 lectures and 4 exercise sessions.
The lectures will be structured as follows (to be updated during the week).

• Lecture 1: Introduction to propositional and first order logic
  In this lecture we introduce the syntax and the semantics of propositional and first order logic.
  Then, we present an Hilbert-Frege axiomatic proof system for first order logic and first-order theories built from first-order languags.
  [Slides ] [Exercises ]


• Lecture 2: Soundness, completeness and other metalogical results
  In this lecture we explore the main metalogical properties of first-order logic.
  Specifically, we introduce the deduction theorem and we will sketch a proof of soundness and completeness and completeness for the logic.
  To conclude, we present compactness, a fundamental corollary of completeness, and its applications.
  [Slides (annotated) ] [Slides ] [Exercises ]


• Lecture 3: Gentzen's sequent calculus
  In this lecture we present Gentzen's sequent calculus, an analytic proof system for first order logic.
  We introduce the main theorem of sequent calculus, the cut-elimination theorem, and illustrate some of its applications.
  [Slides ] [Exercises ]


• Lecture 4: A proof of the cut-elimination theorem
  This lecture is devoted to the proof of the cut-elimination theorem for Gentzen's sequent calculus.
  This theorem is crucial, as it guarantees analyticity of proofs, and requires the definition of non-trivial measures on proofs.
  [Slides (annotated) ] [Slides ] [Exercises ]


• Lecture 5: Beyond classical logic
  In this lecture we introduce formal systems other than classical logic, namely intuitionistic logic and, if time permits, modal logics.
  [Slides (annotated) ] [Slides ]

References

(To be updated)