A Gentle Introduction to Deep Inference

The course will give a gentle introduction to deep inference, which is an intriguing design principle for proof formalisms. The basic idea is that the proof rules which form the building blocks of formal proofs are not restriced to the main connectives of the formulas, but instead can be applied at anywhere deep inside formulas.

In this course, we will provide a clear understanding of the intuitions behind deep inference, together with an exhibition of the properties that deep inference proof systems enjoy. There will be some attention with respect to normalisation, as this is surprisingy different from other more traditional formalisms.

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.

All theses properties also give rise to new notions of proof identity, capturing the "essence" of proof beyond mere rule permutations.

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 work in progress and will appear online here!