Logic and Computation Courses

Advanced Courses

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

Willem Heijltjes and Lutz Straßburger

Week 1, August 3-7, 2020


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.


Connect with us

32nd European Summer School in Logic, Language and Information - ESSLLI 2021
Please send any queries to

  • esslli@uu.nl