Introduction to This LectureThe Petite Modal ZooModal TableauxLecture Notes onModal Tableaux15-816: Modal LogicAndr´e PlatzerLecture 10Februrary 18, 20101 Introduction to This LectureThe Hilbert calculus for modal logic from the last lectures is incredibly sim-ple, but it is not entirely simple to find a proof in it. In this lecture, we in-troduce a modal tableau calculus that is more amenable to systematic proofconstruction and automated theorem proving.Tableaux calculi for modal logic can be found in the work of Fitting[Fit83, Fit88] and the manuscript by Schmitt [Sch03].2 The Petite Modal ZooIn previous lectures, we have mainly seen the propositional modal logicS4 and its Hilbert-style axiomatization. This is, by far, not the only modallogic of interest. The minimal (normal) modal logic is modal logic K. Theaxiomatisation of K is a subset of the axioms of S4 and the same proof rulesof S4; see Figure 1. In fact, normal modal logics share the same proof rules(MP and G) and mostly differ in the choice of axioms.Extensions of logic K are shown in Figure 2.3 Modal TableauxFor proving formulas in propositional modal logic, we develop a tableaucalculus. Tableaux often give very intuitive proof calculi. Here we chooseprefix tableaux, where every formula on the tableau has a prefix σ, whichLECTURE NOTES FEBRURARY 18, 2010L10.2 Modal Tableaux(P) all propositional tautologies(K) (φ → ψ) → ( φ → ψ)(MP)φ φ → ψψ(G)φ φFigure 1: Modal logic KT is system K plus (T) φ → φS4 is system T plus (4) φ → φFigure 2: Some other modal logicsis a finite sequence of natural numbers. In addition, every formula on thetableau has a sign Z ∈ {F, T } that indicates the truth-value we currentlyexpect for the formula in our reasoning. That is, a formula in the modaltableaux is of the formσZAwhere the prefix σ is a finite sequence of natural numbers, the sign Z is in{F, T }, and F is a formula of modal logic. At this point, we understand aprefix σ as a symbolic name for a world in a Kripke structure.Definition 1 (K prefix accessibility) For modal logic K, prefix σ0is accessiblefrom prefix σ if σ0is of the form σn for some natural number n.For every formula of a class α with a top level operator and sign (T orF for true and false) as indicated, we define two successor formulas α1andα2:α α1α2T A ∧ B T A T BF A ∨ B F A F BF A → B T A F BF ¬A T A T Aβ β1β2T A ∨ B T A T BF A ∧ B F A F BT A → B F A T BT ¬A F A F AFor the following cases of formulas we define one successor formulaLECTURE NOTES FEBRURARY 18, 2010Modal Tableaux L10.3ν ν0T A T AF ♦A F Aπ π0T ♦A T AF A F AEvery combination of top-level operator and sign occurs in one of theabove cases. Tableau proof rules by those classes are shown in Figure 3. Atableau is closed if every branch contains some pair of formulas of the formσT A and σF A. A proof for modal logic formula consists of a closed tableaustarting with the root 1F A.(α)σασα1σα2(β)σβσβ1σβ2(ν∗)σνσ0ν01(π)σπσ0π021σ0accessible from σ and σ0occurs on the branch already2σ0is a simple unrestricted extension of σ, i.e., σ0is accessible from σ and no other prefixon the branch starts with σ0Figure 3: Tableau proof rules for QMLThe tableau rules can also be used to analyze F A → ♦A as follows:1 F A → ♦A (1)1 T A (2) from 11 F ♦A (3) from 1stopNo more proof rules can be used because the modal formulas are ν rules,which are only applicable for accessible prefixes that already occur on thebranch. If we drop this restriction, we can continue to prove and close thetableau:1 F A → ♦A (1)1 T A (2) from 11 F ♦A (3) from 11.1 T A (4) from 21.1 F A (5) from 3∗But this is bad news, because the formula A → ♦A that we set out toprove in the first place is not even valid in K. Consequently, the side condi-tion on the ν rule is necessary for soundness!As an example proof in K-tableaux we prove A ∧ B) → (A ∧ B):LECTURE NOTES FEBRURARY 18, 2010L10.4 Modal Tableaux1 F ( A ∧ B) → (A ∧ B) (1)1 T A ∧ B (2) from 11 F (A ∧ B) (3) from 11 T A (4) from 21 T B (5) from 21.1 F A ∧ B (6) from 31.1 F A (7) from 61.1 T A (9) from 4∗ 7 and 91.1 F B (8) from 61.1 T B (10) from 5∗ 10 and 8Let us prove the converse (A ∧ B) → ( A ∧ B) in K-tableaux:1 F (A ∧ B) → ( A ∧ B) (1)1 T (A ∧ B) (2) from 11 F A ∧ B (3) from 11 F A (4) from 31.1 F A (6) from 41.1 T A ∧ B (7) from 21.1 T A (8) from 71.1 T B (9) from 7∗ 6 and 81 F B (5) from 31.1 F B (10) from 51.1 T A ∧ B (11) from 21.1 T A (12) from 111.1 T B (13) from 11∗ 10 and 13Let us try to prove (A ∨ B) → A ∨ B:1 F (A ∨ B) → A ∨ B (1)1 T (A ∨ B) (2) from 11 F A ∨ B (3) from 11 F A (4) from 31 F B (5) from 31.1 F A (6) from 41.2 F B (7) from 51.1 T A ∨ B (8) from 21.2 T A ∨ B (9) from 21.1 T A (10) from 8∗ 10 and 61.1 T B (11) from 8open1.2 T A (12) from 9open1.2 T B (13) from 9∗ 13 and 7This tableau does not close but remains open, which is good news becausethe formula we set out to prove is not valid in K.LECTURE NOTES FEBRURARY 18, 2010Modal Tableaux L10.5ExercisesExercise 1 Prove or disprove using modal tableaux: ♦(A ∧ B) → ♦A ∧ ♦B.Exercise 2 Are the side conditions on the prefixes for the ν∗-rule and the π-rulenecessary or not? Prove or disprove each case.Exercise 3 Use a tableau procedure to prove or disprove the formulas A → ( A ∨ B)and A ↔ Ain the modal logic S4. Explain your solution.Exercise 4 Use a tableau procedure to prove or disprove the formula ♦A → ♦ Ain the modal logic S4. Explain your solution and which difficulties exist in com-parison to classical propositional cases.LECTURE NOTES FEBRURARY 18, 2010L10.6 Modal TableauxReferences[Fit83] Melvin Fitting. Proof Methods for Modal and Intuitionistic Logic. Rei-del, 1983.[Fit88] Melvin Fitting. First-order modal tableaux. J. Autom. Reasoning,4(2):191–213, 1988.[Sch03] Peter H. Schmitt. Nichtklassische Logiken. VorlesungsskriptumFakult¨at f¨ur Informatik , Universit¨at Karlsruhe, 2003.LECTURE NOTES FEBRURARY 18,