Other Modal Tableau Systems
Several other standard modal logics have destructive tableau systems. Sometimes the definition of S ] needs some modification, sometimes variations on modal rules are introduced.
The S ] operations for several logics are given in Figure 5.9 and the modal rules are given in Figure 5.10.Figure 5.11 shows a proof, using the S4 rules, of ?X → ?(?X V Y). Lines 2 and 3 are from 1 by F →. Next an S4 modal rule is applied to F ?(?X V Y) adding 4, while replacing S by S ] eliminates 1 and 3. Now an F V-rule application to 4 adds 5 and 6 and produces a closed tableau, though not an atomically closed one. Continuing, we apply an S4 modal rule again, to 5,
Figure 5.9 Definitionsfor S ]
Figure 5.10 ModalRules
adding 7 while eliminating 4, 5, and 6. Finally, applying the second S4 modal rule to 2 adds 8, and we have atomic closure.
Figure 5.11 S4 Proof of ?X → ? (?X V Y)
5.8