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

ESSLLI 2021 Course — 2nd Week (2-6 August) — 9:45-11:15

Willem Heijltjes & Lutz Straßburger


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.

This course is intended to be advanced. However, we only require some prior knowledge of the sequent calculus or some other formal proof system. And the student should be familiar with the basics of propositional and first-order logic.

The slides for each lecture are linked below. All slides for all lectures in a single pdf are here.

Tentative syllabus

Five 90-minute lectures are split into ten 45-minute units.


Main ESSLLI 2021 webpage

ESSLLI 2021 webpage for this course