I forgot to mention that I have written another paper recently. It’s a proof theory paper, putting down some thoughts on modal proof theory that I formulated when giving the S5 paper around and about in the last six months or so.
In “Comparing Modal Sequent Systems” I look at different ways to understand modal deduction. In particular, I argue that you can understand labelled proof systems – those in which proofs consist of statements annotated with labels, often thought of as denoting ‘possible worlds’ at least in modal proof theory – can be reconceived in such a way as to not really require talk of worlds. When you play close attention to the kind of work done by the labels, it can be understood instead as a different representation of a structural feature of modal deduction.
The point in this paper is a technical one, but the moral is broader than that. The view I argue for in the ‘Invention’ paper feeds off this kind of point. Properly modal deduction involves doing new things in the structure of argument – you can do a kind of supposing (say, ‘hypothetical’ supposing), which has its own interesting behaviour.
Or so I think, anyway. In this paper I look the issue by way of a comparison between labelled deduction and display logic. Display Logic is maligned for being complicated, but not for failing to be ‘structural.’ No-one accuses Display Logic of importing explicit talk possible worlds into proofs. Labelled deduction is criticised for doing exactly that, but it has nice properties. In the paper, I show how you can get from display logic to Labelled Deduction, and thereby get a new view on labelled modal systems, inheriting some of the structural features of display logic, but which has its own kind of simplicity and charm.
Hey. Look at that. Two posts in one day. Even with some philosophico-logical content. I think I can make it three…