Offered through 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


← UNIB10002: Logic, Language and Information | Class Archive | PHIL30043: The Power and Limits of Logic →


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.



To receive updates from this site, you can subscribe to the  RSS feed of all updates to the site in an RSS feed reader, or follow me on Twitter at  @consequently, where I’ll update you if anything is posted.