Proof Theory: Logical and Philosophical Aspects

July 2016

at the 2016 North American Summer School in Logic, Language and Information

This is an intensive class on logical and philosophical issues in proof theory, taught by Shawn Standefer and me at nasslli 2016. We cover cut elimination, some substructural logics, and hypersequents, with a bit of inferentialism and bilateralism mixed in. Here are the slides for each day of the course.

  • Day 1: Foundations. An introduction to the sequent calculus for intuitionistic and classical logic, cut elimination and some of its consequences.
  • Day 2: Substructural Logics. Structural rules in sequent systems; the case of distribution; different substructural logics and their applications; revisiting cut elimination in substructural logics.
  • Day 3: Beyond Sequents. Sequent sytstems for basic modal logics; three ways to move beyond traditional sequent systems—display logic, labelled sequents and tree hypersequents.
  • Day 4: Hypersequents for S5, Actuality and 2D Modal Logics. From tree hypersequents to simple hypersequents for S5; extending simple hypersequents to model actuality and two-dimensional modal logic.
  • Day 5: Semantics. Normative pragmatics; the scope of rules and definitions; between proofs and models; moving beyond propositional logics.

Readings and References


Substructural Logics

Beyond Sequents

Hypersequents for S5, Actuality and 2D Modal Logics



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.