Interpreting and Applying Proof Theories for Modal Logics

March 2012

(with Francesca Poggiolesi) “Interpreting and Applying Proof Theories for Modal Logics,” in New Waves in Philosophical Logic, edited by Greg Restall and Gillian Russell, Palgrave Macmillan, 2012.

Proof theory for modal logic has blossomed over recent years. Many ex- tensions of the classical sequent calculus have been proposed in order to give natural and appealing accounts of proof in modal logics like K, T, S4, S5, provability logics, and other modal systems. The common feature of each of these different proof systems consists in the general structure of the rules for modal operators. They provide introduction and elimination rules for statements of the form □􏰅A (and ◇􏰆A), which show how those statements can feature as conclusions or as premises in deduction. These rules give an account of the deductive power of a modal formula 􏰅□􏰅A (and 􏰆◇􏰆A) in terms of the constituent formula A.

The distinctive feature for the modal operators in contemporary proof systems for modal logics is that the step introducing or eliminating 􏰅􏰅□􏰅A is at the cost of introducing or eliminating some kind of extra structure in the proof. In this way, the proof rules for modal concepts such as 􏰅􏰅□􏰅 run in parallel with the truth conditions for these concepts in a Kripke model, in which the truth of 􏰅􏰅□􏰅A stands or falls with the truth of A, but at the cost of checking that truth elsewhere, at points in the model accessible from the point at which 􏰅􏰅□􏰅A is evaluated.

In this paper we will introduce these recent advances in proof theory for a general audience, and then we will show how they are connected with different—metaphysical and epistemic—conceptions of modality. We will show that these different pictures are nothing but different ways of connecting the statement 􏰅􏰅□􏰅A with the statement A, of showing the significance of modalising. In the light of this result we will draw conclusions about the link between analyticity and modality, and about the nature of a proof system for modal logics.

 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, 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.