An introduction to deep inference

The course will give a basic introduction to deep inference, which is a design principle for proof formalisms in which inference rules can be applied at any depth inside the proof. In this course, we will provide a clear understanding of the intuitions behind deep inference, together with a rigorous account of the properties that deep inference proof systems enjoy, especially in regards to normalisation. Properties that particularly stand out are atomicity, locality, and regularity. Normalisation procedures specific to deep inference allow for new notions of normal forms for proofs, as well as for a general modular cut-elimination theory. Furthermore, the ability to track every occurrence of an atom throughout a proof allows for the definition of geometric invariants with which it is possible to normalise proofs without looking at their logical connectives or logical rules, obtaining a purely geometric normalisation procedure.

This course is intended to be introductory. That means no prior knowledge of proof theory is required. However, the student should be familiar with the basics of propositional logic.

Course notes are online here!

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

• Monday, August 5: Shallow and deep inference
  
  
  • 01: What is a proof system?
    • Which are the properties that we look for?
    • The limitations of 20th century proof theory
  
  
  • 02: What is deep inference?
    • Basic description and motivations
    • Comparison to the traditional formalisms


• Tuesday, August 6: Full dive into deep inference
  
  
  • 03: Properties of deep inference
    • Locality and atomicity
    • Duality and regularity
  
  
  • 04: Formalisms, derivations, and proofs
    • The calculus of structures
    • Open deduction
    • Operations on derivations
    • Translating between deep inference systems and sequent calculus


• Wednesday, August 7: Normalisation
  
  
  • 05: Decomposition
    • First Decomposition Theorem: From creation to destruction
    • Second Decomposition Theorem: Finding the core of a proof system
  
  
  • 06: Splitting
  • Shallow splitting
  • Context reduction


• Thursday, August 8: The geometry of deep inference
  
  
  • 07: Atomic flows
    • Where connectives mean nothing
    • Local and global proof transformations
    • Taming proofs and breaking paths
  
  
  • 08: Combinatorial proofs
  • Formulas without syntax
  • Proofs without syntax


• Friday, August 9: Subatomic logic
  
  
  • 09: Subatomic splitting
  • Subatomic proofs: composing even further
  • General splitting: one theorem to rule them all
  
  
  • 10: Subatomic decomposition
    • General rewriting rules: permuting nestings of contractions
    • Cycle elimination: how to stop going in circles

Main ESSLLI 2019 webpage

ESSLLI 2019 webpage for this course

Deep inference webpage maintained by Alessio Guglielmi