Proof Theory

June 2024 COMING SOON

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.