Modal Tableaus for K
The classical propositional language we have been using is now enhanced with ?. The 0 could easily be added too, but it plays no special role when studying justification logics, so we omit it.
There are several varieties of modal tableaus. Here we will use what are called a destructive version. The name comes from the fact that certain rules cause branch information to disappear. Such tableaus exist for K, T, D, D4, K4, and S4, among other familiar logics, but not for S5. We will sketch rules for these systems in the next section, and for K here. We begin with a signed analog of Definition 4.6.Definition 5.15 (Modal Sharp Operation, Signed Version) For a set S of signed modal formulas, le
There is only one modal rule for K, given in Figure 5.7, in addition to the classical propositional rules given earlier. This rule is applicable to a branch containing
with S being the set of other formulas on the branch. The entire branch is replaced with a new branch consisting of the members of S ], and FX. Note that information is lost passing from S to S ] —the reason why such tableaus are called destructive.
Figure 5.7 Modal K Rule
Figure 5.8 shows a tableau proof using the K-rules,
Y). Itbegins with several classical rule applications. After 5 has been added, we apply the modal K rule on 3. We add F XλY, but we must replace the remaining set S of signed formulas with S ]. This modifies the branch to consist of signed formulas 6, 7, and 8. Here 1, 2, and 3 have been deleted, 4 and 5 replaced by 6 and 7, then 8 added to in place of 3. We have drawn a line to indicate the replacement of the old branch contents by the new ones. Now 8 causes branching and yields a closed tableau.
With classical propositional tableaus, any order of rule application must produce a proof if one exists, as long as eventually every applicable rule has been applied. This is not the case for K. If both F ?X and F ? Y are present on the same branch, applying a rule to one eliminates the other, and it may be that only one of the two possibilities will lead to a proof. Backtracking is critical to proof search using modal tableaus. Because the number of backtracking possibilities is always bounded, a systematic search for a K tableau proof allowing backtracking will provide a decision procedure for that logic.
5.7