Proof Theory

June 2024

at Nordic Logic Summer School 2024

This is an intensive class on logical and philosophical issues in proof theory, taught at nls2024 as part of the Reykjavik Summer of Cool Logic 2024.

In this course, I’ll introduce natural deduction and sequent calculus for classical, constructive and substructural logics, motivating and explaining how key results (normalisation for natural deduction proofs and cut elimination for sequent calculus derivations) may be proved, and how these interact with the presence or absence of the structural rules of weakening and contraction. We will also take a look at different proof systems designed to model modal and other intensional logics. Along the way we will see (1) the difference between multiplicative and additive rules for connectives (2) different ways to understand harmony between introduction and elimination rules (or left and right rules in the sequent calculus) (3) the ways in which rules for a connective may be understood as defining the concept introduced; (4) the connection between proof dynamics, dialogue and speech acts; (5) the relationship between proof search and model construction, and (6) connections between structural rules, paradoxes and fixed points.

Class Resources

If you are attending the class, you can download the (password-protected, for the moment) class notes here. I’ll upload the slides after each class.

• Monday: Natural Deduction. (Slides | Reading: Chapter 1.)
• Tuesday: Sequent Systems. (Slides | Reading: Chapters 2 and 4.)
• Wednesday: Positions, Models and More. (Slides | Reading: Chapters 3, 5 and 6.)
• Thursday: Modal Logic. (Slides | Reading: Francesca Poggiolesi and Greg Restall “Interpreting and Applying Proof Theories for Modal Logics”, in New Waves in Philosophical Logic, edited by Greg Restall and Gillian Russell, Palgrave, 2012.)