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.
If you’re a logician, I’d love to know what you think of it. Download it from here and leave a comment. I’ve submitted it for presentation at AiML 2006.
Hey. Look at that. Two posts in one day. Even with some philosophico-logical content. I think I can make it three…
