Does anyone know where I can find a decent natural deduction presentation of modal logic. Girle's Modal Logic and Philosophy as well as Konyndyk's Modal Logic both present proof theory in a lot more detail than Chellas, or Hughes and Cresswell. But what Girle and Konyndyk call "natural deduction" would cause someone interested in proofs to gnash their teeth.
I'm looking for a treatment that explores how much you can get with the idea that modal operators get their meaning from introduction and elimination rules, and that these rules should be answerable to certain proof theoretic constraints (the kind of thing Catarina notes in this cool post that is being now explored with dialogic approaches to logic, e.g. conservative extension requirements showing soundness of adding both the intro and elimination rule, normalizability as a kind of soundness showing that the elimination rule is not too strong given the introduction rule, and the ability to prove uniqueness of the operator in the logic as a kind of completeness to show that the eliminatino rule is not too weak given the introduction rule).
Restall has a great paper on modal logic and sequent calculi that I'm reading with some students in an independent study in a couple of weeks, but I don't know what's out there exploring modal logic from a proper natural deduction standpoint.
Intuitively, you should be able to index steps in the proofs to worlds, constraints on the world indexes for possibility elimination and necessity introduction that are analogous to the constraints on arbitrary names for existential elimination and universal introduction. If the background logic is classical, I assume that you would get S5 doing this, and you probably get an interesting logic if you treat the quantification over worlds intuitionistically (someone has to have developed this). But the only example I've found of anything like this world indexing of proofs in textbooks is via tree proofs (I don't mean Prawitz style natural deduction trees, but the ones where you simplify the formula and then block out nodes).
So if anybody can name some papers or even better a textbook that takes the proof theory of modal logic seriously (again- intro and elim rules such that tonk like issues can be raised).
[Addendum: Oops, I just noticed that Prawitz' classic book Natural Deduction (which I think is the first presentation of normalizability as a proof theoretic soundness requirement on elimination rules) has a very brief discussion of modal logic; I'm going to go read this and then post later if it is helpful. At this point it looks pretty provisional though.]
Recent Comments