Suppes–Lemmon-Style ◇-Introduction and -Elimination Rules for Modal Logics?

Question

I'm trying to find natural-deduction introduction and elimination rules for the diamond (◇) in popular modal logics (e.g., K, T, S4, and S5) in the style of Suppes and Lemmon, where on each line of the proof you have a dependency set, a line number, a formula, and a citation, e.g.,

{1} 1. P   Premise
{1} 2. P ∨ Q  1 ∨I

Satre (1972) is the closest thing I've found; he gives a bunch of rules for introducing or eliminating the box (□) in the abovementioned logics (and many more besides), but unfortunately doesn't give any for the diamond. An earlier poster on this site suggested ◇-introduction and -elimination rules for S5, but formulated them in terms of subproofs—which aren't a thing in the Suppes and Lemmon style—and only gave them for S5.

If there's a textbook that gives such rules, that'd be ideal, especially if it has accompanying exercises to practice using them, but it's fine if someone's just able to formulate them themselves.

Answer 1

It is possible to formalise modal logics using natural deduction rules, but it is not as simple as it is for elementary classical logic. You won't be able to avoid relying on subproofs or something equivalent.

One of the nice things about classical propositional logic is that it is structurally complete, which means that all of its admissible rules are derivable rules, and so there is no distinction between a rule of inference and a rule of proof. This is not generally the case with modal logics. For example, in the base normal system K, the following rule is admissible but not derivable:

  □P
 ----
   P

So, while this can serve as a □-elimination rule, we have to be careful how it is used. □P must be derivable in a subproof. Whereas in T, S4 and S5 this is a derivable rule and can be used without restriction.

Similarly, the necessity introduction rule is admissible but not derivable in K, T, S4, or S5.

   P
 ----
  □P

So this can be used as a □-introduction rule, but only when P is either a theorem of the underlying logic or is derivable without assumptions in a subproof.

In standard modal logics we don't need separate rules for ◇ because we have the equivalence relations:

  ◇P  <===>  ¬□¬P      and     □P  <===>  ¬◇¬P 

There are relatively few sources that provide natural deduction systems for modal logics. There is some material in Rod Girle, Modal Logics and Philosophy (2nd edition, 2009), pp. 68-73.