A Cut-Free Sequent System for Two-Dimensional Modal Logic, and why it matters

November 2012

“A Cut-Free Sequent System for Two-Dimensional Modal Logic—and why it matters,” Annals of Pure and Applied Logic 2012 (163:11) 1611–1623


The two-dimensional modal logic of Davies and Humberstone is an important aid to our understanding the relationship between actuality, necessity and a priori knowability. I show how a cut-free hypersequent calculus for 2d modal logic not only captures the logic precisely, but may be used to address issues in the epistemology and metaphysics of our modal concepts. I will explain how use of our concepts motivates the inference rules of the sequent calculus, and then show that the completeness of the calculus for Davies–Humberstone models explains why those concepts have the structure described by those models. The result is yet another application of the completeness theorem.

(This paper was awarded a Silver Medal for the Kurt Gödel Prize in 2011.)

 download pdf

You are welcome to download and read this document. I welcome feedback on it. Please check the final published version if you wish to cite it. Thanks.


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. 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  @consequently@scholar.social, where most updates are posted.


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