Proof Theory
Introductory course at MGS 2022
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)
Gianluca Curzi, Marianna Girlando @ MGS 2022