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.
As additional course material, we suggest the course notes for the
ESSLLI 2019 course and the
ESSLLI 2021 course.
Syllabus
Five 90-minute lectures are split into 30-minute or 45-minute units.
-
Monday, July 28: Introduction. Shallow inference and deep inference.
- 01: Some 20th century proof formalisms (handout+slides)
-
Hilbert/Frege systems
-
Natural deduction
-
Sequent calculus
- 02: Open deduction: A 21st century proof formalism (handout+slides)
-
Locality and atomicity
-
Duality and regularity
-
Tuesday, July 29: Normalization
- 03: Cut elimination in the sequent calculus (handout+slides)
-
What is a cut? And why do we want to eliminate it?
-
Cut reduction
- 04: Cut elimination in open deduction for classical logic (handout+slides)
-
Atomicity breaks everything
-
Atomicity fixes everything
- 05: Cut elimination via Splitting and Decomposition (handout+slides)
-
Splitting
-
Context reduction
-
Decoposition
-
Wednesday, July 31: The geometry of deep inference
- 06: Atomic flows (slides)
-
Where connectives mean nothing
-
Local and global proof transformations
-
Taming proofs and breaking paths
- 07: Combinatorial proofs (handout+slides)
-
Formulas without syntax
-
Proofs without syntax
-
Thursday, August 1: Proof complexity of deep inference
- 08: Introduction to proof complexity
(handout+slides)
-
Again: What is a proof system?
-
p-simulation
- 09: Comparing different proof systems (slides)
-
From Frege systems to deep inference
-
Contraction and cocontraction
- 10: Other Proof compression mechanisms (handout+slides)
-
Cut
-
Extension and substitution
-
Contraction and cocontraction
-
Friday, August 2: The future of deep inference
- 11: Subatomic proof theory (slides)
-
from splitting atoms to subatomic inference rules
-
General splitting: one theorem to rule them all
- 12: Open problems (handout+slides)
Links
-->