Teachers: Matteo Acclavio and Paolo Pistone

Classes are evey morning from 11h to 13h

- What is a proof?
- Two approaches to the problem of Proof Identity
- What is a proof system?
- Natural Deduction, Sequent Calculus and rule permutations.

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.

- Ideas and Results in Proof Theory
- Hilbert's Twenty-Fourth Problem
- The Problem of Proof Identity, and why computer scientists should care about Hilbertâ€™s 24th problem

- How much information is needed?
- Multiplicative Linear Logic, Proof nets, and units
- Are structural rules canonical?
- Canonicity of structural rules

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.

- Proof nets for MLL
- Proof nets for MLL (linear time correctness criterion)
- No proof nets for MLL with units
- Slice nets (MALL)
- Conflic nets (MALL)

- Is natural deduction canonical?
- Natural deduction, normalization and canonicity
- What is a Denotational Semantics?
- Game semantics for Intiotionistic Propositional Logic

- Deciding equivalence in LJ (with conjunction)
- Game Semantic (introduction)
- Game Semantic (as presented, forget about modalities)

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.

- Why normalization is not suitable for proof equivalence in classical logic?
- Reducing non-determinism via Focusing
- How much non-determinism can we get rid of?
- Combinatorial Proofs for Classical Logic

- Focusing Gentzen's LK proof system (recorded talk)
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- ESSLLI 2021 course on Combinatorial Proof

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.

- What about quantifiers?
- Proof equivalence in first and second order logic
- Why computer scientist should care about proof equivalence?
- Applications to real world problems

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.