From Proof Nets to Combinatorial Proofs — A new approach to Hilbert’s 24th problem

LoCo Advancedweek 2

each day

Lecturers:
Willem Heijltjes (University of Bath)
Lutz Straßburger (Inria Saclay & Ecole Polytechnique)

Website: https://www.lix.polytechnique.fr/~lutz/orgs/ESSLLI2021-course.html

Abstract: Hilbert's 24th problem is the question of when two proofs are the same. The problem is as old as proof theory itself, but there is still no satisfactory solution. The main reason for this is the syntactic bureaucracy of formal proof systems. In order to reduce this bureaucracy, Girard introduced proof nets, a certain kind of graphs, which provide a solution for some fragments of linear logic, but not for classical logic. For this reason, Hughes introduced combinatorial proofs, which can be seen as a combination of a proof net and a skew fibration. The common feature of proof nets and combinatorial proofs is that they are not syntactic objects but combinatorial objects. The interplay between syntax and combinatorics will be the main topic of the course.