All of the inference rules we learned in propositional logic (modus ponens, modus tollens, etc.) also hold in modal logic. Likewise, all of the equivalence rules of propositional logic (double negation, commutation, etc.) hold in modal logic as well. However, modal logic adds some new inference and equivalence rules. As before, we can state these inference and equivalence rules using variables like x and y to stand for any WFF. Here are four new equivalence rules for modal logic:
A simple way to remember all four of these equivalences is to visualize the tilde jumping over the box or the diamond and, as it does so, transforming the box into a diamond or vice versa. For example, in the first equivalence rule above, the tilde moves from the left side of the diamond to the right side, thereby transforming the diamond into a box. Similarly, in the second equivalence rule, the tilde jumps from the right side of the diamond to the left side, again turning the diamond into a box. In the third rule, when the tilde jumps over the diamond it encounters another tilde on the other side, and the two tildes cancel each other out (as in the double negation rule), but the jumping tilde still transforms the diamond into a box. Likewise, in the last rule, one of the two tildes jumps over the box and cancels with the other tilde, and the box turns into a diamond.
(P ⊃ ◇~Q) is equivalent to (P ⊃ ~□Q) by the second equivalence rule above. As with the equivalence rules for propositional logic, equivalent formulas can be substituted for one another even when they appear as components of a larger WFF. In this case, the consequent of the conditional is replaced by an equivalent formula.
(~◇~A ∨ B) is equivalent to (□A ∨ B) by the third equivalence rule above.
◇(P ≡ ~Q) is equivalent to ~□~(P ≡ ~Q) by the fourth equivalence rule above.
Modal logic adds some new inference rules as well. For example, a premise stating that some proposition is necessarily true allows us to infer that the claim is possibly true: □x entails ◇x. However, several different systems of modal logic have been developed for a variety of applications in professional philosophy, and some of the inference rules differ from one system to another! For example, in a system of modal logic called S5, the proposition ◇□x entails □◇x, but this inference is invalid in system S4. For now, we’ll keep things simple and use only the inference rules of propositional logic, which are valid in all of the commonly employed systems of modal logic.