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

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.

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

• Monday, August 2: The Beginning
  
  
  • 01: Overview and Motivation (slides)
    • What is Hilberts 24th problem?
    • The limitations of 20th century proof theory
  
  
  • 02: What are proof nets? (slides)
    • Curry-Howard Isomorphism
    • Sequent calculus versus proof nets


• Tuesday, August 3: Full dive into multiplicative linear logic
  
  
  • 03: Cographs and co (slides)
    • Graphs and cographs
    • Perfect matchings and handsome proof nets
  
  
  • 04: Deep inference (slides)
    • Translating between deep inference systems and sequent calculus
    • From deep infernce to proof nets


• Wednesday, August 4: Resource management in proofs
  
  
  • 05: Additive linear logic (slides)
    • Sequent calculus and proof nets
    • Deep inference
  
  
  • 06: Skew fibrations (slides)
    • Fibrations and skew fibrations
    • Contraction and weakening


• Thursday, August 5: Classical logic — Putting things together
  
  
  • 07: propositional logic (slides)
    • Combinatorial proofs for classical proposional logic
    • Decomposition theorems
  
  
  • 08: First-order logic (slides)
    • Combinatorial proofs for classical first-order logic
    • Decomposition theorems
  
  
• Friday, August 9: Intuitionistic logic
  
  
  • 09: Intuitionistic combinatorial proofs (slides)
    • Arenas and arena nets
    • Skew fibrations on arenas
    
    
  • 10: Normalization (slides)
    • Cut-trees
    • Reducibility candidates

Main ESSLLI 2021 webpage

ESSLLI 2021 webpage for this course