Teachers: Matteo Acclavio and Paolo Pistone
Classes are evey morning from 11h to 13h
In this class we discuss the notion of proof and how they can be formalized. After underlying the importance of defining a notion of proof equivalence, we provide the two main approaches to this problem we will explore during the course. We recall the definition of proof system by Cook-Reckhow and the sequent calculi and natural deduction systems for both classical and intuitionistic logic. We then analyze the standard rules permutations we can perform on sequent calculus derivations.
We show the Multiplicative Linear Logic and how we can represent proofs using proof nets. We show their canonicity w.r.t. sequent calculus derivations. We show then show that as soon as units or structural behaviors are included in a system, then canonicity may become impossible to achieve.
We show the canonicity of disjuntion-free fragment natural deduction with respect normalization and generality. Moreover, in presence of disjunction we can make obtain canonicity with respect to normalization but not with respect to generality. We then define the notion of denotational semantics. We show how a denotational semantics can be easily defined in term of quotient, we show how Game Semantics provides a concrete model for such a semantics.
We show the impossibility of having a non-trivial denotational semantics for classical logic by presenting Lafont critical pairs and Joyal's argument. We then present some refinement of sequent calculi allowing to reintroduce canonicity by reducing the non-determinism in proof search. We conclude by introducing the syntax of combinatorial proofs for classical logic, a graphical syntax suitable to provide a canonical representation of proofs. We discuss which rule permutations are captured by this syntax and we discuss the extension of this syntax to other logic.
We introduce first and second order quantifiers, and the calculi for first and second order classical and intuitionistic logic. We show the additional challenges in proof equivalence for these logics, and the partial results in the literature. We conclude the course by illustrating applications of proof equivalence to verification, interoperability of theorem provers and suggests the current trends in proof theoretical approaches to programming language theory.