Proof Theory


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.


I’m Greg Restall, and this is my personal website. I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews, and the Director of the Arché Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology I like thinking about – and helping other people think about – logic and philosophy and the many different ways they can inform each other.


To receive updates from this site, subscribe to the RSS feed in your feed reader. Alternatively, follow me at, where most updates are posted.


This site is powered by Netlify, GitHub, Hugo, Bootstrap, and coffee.   ¶   © 1992– Greg Restall.