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