Introduction to Modal and Temporal Logic © Rajeev Gore Automated Reasoning Group Computer Sciences Laboratory Australian National University http://arp.anu.edu.au/^rpg Raj eev.Gore@anu.edu.au 6 December 2007 Version 1.5 Tel: ext. 58603 Introduction to Modal and Temporal Logics 6 December 2007 1 History: Logic of Necessity and Possibility Classical logic is truth-functional: truth value of larger formula determined by truth value(s) of its subformula(e) via truth tables for A, v, -, and —. Lewis 1920s: How to capture a non-truth-functional notion of "A Necessarily Implies B"? (A — B) Take A —< B to mean "it is impossible for A to be true and B to be false" Write PA for "A is possible" then: -PA is "A is impossible" -P-A is "not-A is impossible" NA := -P-A "A is necessary" A —< B := N(A — B) = -P-(A — B) = -P-(-A V B) = -P(A A -B) Modal Logic: "possibly true" and "necessarily true" are modes of truth Introduction to Modal and Temporal Logics 6 December 2007 2 Preliminaries Directed Graph (V, E): where V = {v0, vi, • • • } is a set of vertices E = {(s1, t1), (s2, t2), • • • } is a set of edges from source vertex s$ e V to target vertex ^ e V for i =1,2, • • •. Cross Product: V x V stands for {(v, w) | v e V, w e V} the set of all ordered pairs (v, w) where v and w are from V. Directed Graph (V, E): where V = {v0, v1? • • • } is a set of vertices and E c V x V is a binary relation over V. Iff: means if and only if. Introduction to Modal and Temporal Logics 6 December 2007 3 Logic = Syntax and (Semantics or Calculus) Syntax: formation rules for building formulae p, • • • for our logical language Assumptions: a (usually) finite collection r of formulae Semantics: p is a logical consequence of r (r |= p) Calculi: p is derivable (purely syntactically) from r (r V p) Soundness: If r V p then r |= p Completeness: If r |= p then r V p Consistency: Both r V p and r I—p should not hold for any p Decidability: Is there an algorithm to tell whether or not r |= p ? Complexity: Time/space required by algorithm for deciding whether r | p ? Introduction to Modal and Temporal Logics 6 December 2007 4 Syntax of Modal Logic Atomic Formulae: p :: = p0 | pi | p2 (Atm) Formulae: p ::= p | — p | ()p | []p | p A p | p V p | p — p Examples: []po — p2 []p3 — [][]pi [](pi — P2) — (([]pi) — ([]P2)) Variables: p, q, r stand for atomic formulae while p, ^ possibly with subscripts stand for arbitrary formulae (including atomic ones) Schema/Shapes: []p — p []p — [][]p [](p — ^) — ([]p — []^) Schema Instances: Uniformly replace the formula variables with formulae Examples: []p0 — p0 is an instance of []p — p but []p0 — p2 is not Formula Length: number of logical symbols, excluding parentheses, where length(p0) = length(p1) = • • • =1 Example: length([]p0 — p2) = 4 Introduction to Modal and Temporal Logics 6 December 2007 5 Kripke Semantics for Logical Consequence Motivation: Give an intuitive meaning to syntactic symbols. Motivation: Give the meaning of V is true" Motivation: Define a meaning of V is a logical consequence of r" (r |= (/?) Goal: Prove some interesting properties of logical consequence. Introduction to Modal and Temporal Logics 6 December 2007 6 Kripke Semantics for Logical Consequence Kripke Frame: directed graph (W, R) where W is a non-empty set of points/worlds/vertices and R c W x W is a binary relation over W Valuation: on a Kripke frame (W, R) is a map # : W x Atm — {t, f} telling us the truth value (t or else f) of every atomic formula at every point in W Kripke Model: (W, R, #) where # is a valuation on a Kripke frame (W, R) Example: If W = {wo, wi, W2} and R = {(wo, wi), (wo, W2)} and ,p3) = t then (W, R, #) is a Kripke model as pictured below: #(wo,p) = f for all p g Atm #(wi ,p) = f for all p = P3 g Atm #(w2,p) = f for all p g Atm #(wo, ()pi) = ? #(wo, []pi) = ? wo wi w2 Introduction to Modal and Temporal Logics 6 December 2007 7 Kripke Semantics for Logical Consequence Given some model (W, R, #) and some w e W, we compute the truth value of a non-atomic formula by recursion on its shape: #0, -p) t if #(w,p) = f f otherwise t if #(w, p) = t and #(w, |) = t f otherwise t if #(w, p) = t or #(w, |) = t f otherwise t if #(w, p) = f or #(w, i|) = t #(w,p - ^) = | f otherwise (-p V1} Intuition: classical connectives behave as usual at a world (truth functional) Introduction to Modal and Temporal Logics 6 December 2007 8 Kripke Semantics for Logical Consequence Given some model (W, R, #) and some w e W, we compute the truth value of a non-atomic formula by recursion on its shape: ( o ) _ ft #(v,, either tf(w, 0. Induction Step: If

G VF.u> lh p 3w G VF.w 1/ p in a frame $ forces ip £¥p lh p Classicality: either • ¥ p or else • ¥ p holds for • g {w, M, F} Exercise: Work out the negation of each fully e.g. M ¥ p is 3w g W.w ¥ -p Either w ¥ p or else w ¥—p holds (Lemma 1) But this does not apply to all: e.g. either M ¥ p or else M ¥ -p is rarely true. W ¥ p meaning "every frame built out of given W forces p" is not interesting Introduction to Modal and Temporal Logics 6 December 2007 12 Various Consequence Relations Let k be the class of all Kripke models, and m = (W, R, #) a Kripke model Let K be the class of all Kripke frames and let F be a Kripke frame Let r be a set of formulae, and

G w.ii; lh ip in a frame f forces ip w.(f,#) ih Let • \h r stand for g \h ^ (• g {w, m, F}) World: every world that forces r also forces

* w \h Model: every model that forces r also forces

* m \\- y> Frame: every frame that forces r also forces

* F \l- ^ Introduction to Modal and Temporal Logics 6 December 2007 13 Various Consequence Relations Let k be the class of all Kripke models, and m = (W, R, #) a Kripke model Let K be the class of all Kripke frames and let F be a Kripke frame. Let r be a set of formulae, and

G W.iü lh ip zlw G VF.w 1/ (/? in a frame F forces ip Flhcp W.(F,#) lh

l/y> Let • lh r stand for v0 g lh <0 (• g {w, m, F}) World: vw g W.w lh r w lh

* F lh

where []0y = y and []ny = [] []n-1y (See Kracht for details) e.g. p0 |= []p0 implies 0 |= (p0 A []p0) — []p0 so n = 1 for this example Introduction to Modal and Temporal Logics 6 December 2007 19 Summary: Logic = Syntax and Semantics Atomic Formulae: p :: = p0 | p1 | p2 (Atm) Formulae: } = {y> | vf e k.f lh y>} Introduction to Modal and Temporal Logics 6 December 2007 20 Lecture 2: Hilbert Calculi Motivation: Define a notion of deducibility "p is deducible from r" Requirement: Purely syntax manipulation, no semantic concepts allowed. Judgment: r h p where r is a finite set of assumptions (formulae) Read r h p as "p is derivable from assumptions r" Soundness: If r h p then r |= p If p is derivable from r then p is a logical consequence of r Completeness: If r |= p then r h p If p is a logical consequence of r then p is derivable from r Goal: Deducibility captures logical consequence via syntax manipulation. Introduction to Modal and Temporal Logics 6 December 2007 21 Hilbert Calculi: Derivation and Derivability Assumptions: finite set of formulae accepted as derivable in one step (instantiation forbidden) Axiom Schemata: Formula shapes, all of whose instances are accepted unquestionably as derivable in one step (listed shortly) Rules of Inference: allow us to extend derivations into longer derivations Judgment: r h p where r is a finite set of assumptions (formulae) x Judgmenti ... Judgment™ .... x premisses Rules: (Name) ---^-^-- (Condition) -—=—:— Judgment conclusion Read as: if premisses hold and condition holds then conclusion holds Rule Instances: Uniformly replace formula variables and set variables in judgements with formulae and formula sets Introduction to Modal and Temporal Logics 6 December 2007 22 Hilbert Derivability for Modal Logics Assumptions: finite set of formulae accepted as derivable in one step (instantiation forbidden) Axiom Schemata: Formula shapes, all of whose instances are accepted unquestionably as derivable in one step (listed shortly) (Ax) —— ip is an instance of an axiom schema rVp Rules of Inference: allow us to extend derivations into longer derivations Modus Ponens (MP) r h ^ rhy?^^ r v ip Necessitation (Nec) J~, ^~rf r V []p Introduction to Modal and Temporal Logics 6 December 2007 23 Hilbert Derivability for Modal Logics (Id) —— p e r (Ax) —— ip is an instance of an axiom schema r h p r h p ,R-r^x r h p r h p — ^ , r h p (MP) rh/ (Nec) rF[fe Rule Instances: Uniformly replace formula and set variables with formulae and formula sets Derivation of po from assumptions ro: is a finite tree of judgments with: 1. a root node ro h po 2. only (Ax) judgment instances and (Id) instances as leaves (sic!) 3. and such that all parent judgments are obtained from their child judgments by instantiating a rule of inference Introduction to Modal and Temporal Logics 6 December 2007 24 Hilbert Calculus for Modal Logic K Axiom Schemata: PC: (/? — (0 — — (0 — 0) — ((v — 0) — — £)) K: — 0) — (D(P — []0) How used: Create the leaves of a derivation via: (Ax) —— ip is an instance of an axiom schema r h v V A 0 := —— —0) V V 0 := (—v — 0) V 0 := — 0) A (0 — Introduction to Modal and Temporal Logics 6 December 2007 25 Hilbert Derivations: Examples Let r0 = {po,Po — Pi} and (/?0 = Usually omit braces. Below is a derivation of from {p0,p0 — (Id) (Id) p0,p0 — p1 h p0 p0,p0 — p1 h p0 — p1 (MP) p0,p0 — p1 h p1 (Nec) p0,p0 — p1 h A derivation of ^0 from assumptions r0 is a finite tree of judgments with: 1. a root node r0 h ^0 2. only (Ax) judgment instances and (Id) instances as leaves 3. and such that all parent judgments are obtained from their child judgments by instantiating a rule of inference Introduction to Modal and Temporal Logics 6 December 2007 26 Hilbert Derivations: Examples Let r0 _ {p0,p0 — pi} and y 0 _ Usually omit braces. Below is a derivation of from {p0,p0 — p0,p0 — pi - p0 (Id) p0,p0 — pi - p0 — pi p0,p0 — pi - pi p0,p0 — pi - (Nec) (Id) (MP) (Nec) r h (f r :_ {p0,p0 — pi} Introduction to Modal and Temporal Logics 6 December 2007 27 Hilbert Derivations: Examples Let r0 = {po,Po — pi} and p0 = Usually omit braces. Below is a derivation of from {p0,p0 — p0,p0 — pi h p0 (Id) p0,p0 — pi h p0 — pi p0,p0 — pi h pi p0,p0 — pi h (Nec) (Id) (MP) (MP) r h p r h p — ^ Introduction to Modal and Temporal Logics 6 December 2007 28 Hilbert Derivations: Examples Let r0 = {p0,p0 — p1} and ^0 = []p1. Usually omit braces. Below is a derivation of []p1 from {p0,p0 — p1}. (Id) (Id) £0p0 — p1 - p0 p0,p0 — p1 - p0 — p1 -(MP) p0,p0 — p1 - p1 -(Nec) p0,p0 — p1 - []p1 (id)—^er (id)—^er r := {p0,p0 — p1} r := {p0,p0 — p1}

0. Ind. Step: Suppose r h i/j has a derivation of length k. Bottom-most rule? MP: So both r h p and r h p — i/j are shorter than k. By IH r = p — ^ and r = p. But if w \\ p — i/j and w \\ p then w \\ i/j, hence r = ^ Nec: Then we know that r h i/j has length shorter than k. By IH we know r = <0. But if r = <0 then r = []^ by Eg 4. Introduction to Modal and Temporal Logics 6 December 2007 32 Completeness: all semantic consequences are derivable Theorem: if r _ y then r - y Proof Method: Prove contrapositive, if r - y then r _ y Proof Plan: Assume r - Show there is a K-model Mc _ (Wc, Rc, #c) such that Mc \h r and Mc \f y (i.e. 3w e Wc.w \\- - y) Technique: is known as the canonical model construction Local Consequence: Write X - y iff there exists a finite subset {V^, V2, • • • , Vn} C X such that 0 - A V2 a • • • A Vn) — y Exercise: if X — y then X - y by (MP) on X - A(VO and X -A(VO — y Set X is Maximal: if VVV e X or -V e X Set X is Consistent: if both X - V and X - -V never hold, for any V Set X is Maximal-Consistent: if it is maximal and consistent. Introduction to Modal and Temporal Logics 6 December 2007 33 Lindenbaum's Construction of Maximal-Consistent Sets Lemma 6 Every consistent r is extendable into a maximal-consistent X* d r. Proof: Choose an enumeration pi,p2,p3, of the set of all formulae. Stage 0: Let X0 := r Stage n > 0: X •={ Xn-1 U {pn} if Xn-1 V pn y " n' \ Xn-1 U {-pn} otherwise Stage u: X* := Uu=0 Xn Question: Every Stage is deterministic so why is X* not unique ? (choice) Not Effective: Relies on classicality: either Xn-1 V pn or Xn-1 I/i pn is true, but does not say how we decide the question. Exercise: Why is having both Xn-1 Vl pn and Xn-1 Vl -pn impossible ? Introduction to Modal and Temporal Logics 6 December 2007 34 Lindenbaum's Construction of Maximal-Consistent Sets Lemma 7 Every consistent r is extendable into a maximal-consistent X* d r. Proof: Choose an enumeration p15p2,p3, of the set of all formulae. Stage 0: Let X0 := r Stage n > 0: X •={ Xn-1 U {pn} if Xn-1 Vl pn y " n" \ Xn-1 U {-pn} otherwise Stage u: X* := Uu=0 Xn Chain of consistent sets: X0 c X1 c • • • Maximality: Clearly, for all p either p g X* or else -p g X* X* is consistent: Suppose for a contradiction that X* is inconsistent. Thus X* Vl ip and X* Vl -ip for some p. Hence ip g X$ and -ip g Xj for some i and j. Let k := max{i, j}. Then Xk Vl ip by (Id) and Xk Vl -ip by (Id). Contradiction since Xk is consistent. Introduction to Modal and Temporal Logics 6 December 2007 35 The Canonical Model Mr = (Wc, Rc, #c) Wc := {X* | X* is a maximal-consistent extension of r} = 0 w Rc v iff {^ 1 []^ G w} C v ^c(w,p) := { ^ othe^rWse Claim: wRcv iff {()(/? | ^ G v} C w Proof left to right: Suppose wRcv and {()(/? | ^ g v} C w. Hence, there is some ^ g v such that ()

e w iff p e w and ?/> e w v: p v ?/> e w iff p e w or i/j e w p — ?/> e w iff p e w or ^ e w []: []p e w iff Vv e w.wRcv p e v ()p e w iff 3v e w.wRcv & p e v Introduction to Modal and Temporal Logics 6 December 2007 37 The Canonical Model Mr = (Wc, Rc, #c) Wc := {X* | X* is a maximal-consistent extension of r} = 0 w Rc v iff {p 1 []p G w} c v ^c(w,p) := j t o^rJse Claim: p A V g w iff p g w and V g w Proof right to left: Suppose p A V g w and p G w. Then -p g w. Note (p A V) — p G w since 0 H/ (p A V) — p by PC (exercise) Exists k with Xk H/ -p, and Xk H/ p A V, and Xk H/ (p A V) — p, by (Id). Then Xk H p by (MP) Contradiction. Proof left to right: Suppose p g w and V G w and p A V G w. i.e. (p — -V) G w since p A V := -(p — -V) i.e. exists k such that Xk H/ p and Xk H/ p — -V and Xk H/ V by (id) Then Xk H -V by (MP) Contradiction Introduction to Modal and Temporal Logics 6 December 2007 38 The Canonical Model Mr = (Wc, Rc, #c) Wc := {X* | X* is a maximal-consistent extension of r} = 0 w Rc v iff {^ 1 []^ g w} c v ^c(w,p) := { t ot^nwse Claim: []p g w iff Vv G Wc.(wRcv =>* p G v) Proof left to right: Suppose []p g w and Vv g Wc.wRcv ^ p g v i.e. []p G w and 3v G Wc.wRcv & p G v i.e. []p g w and 3v g Wc.p G v & p G v Contradiction. Introduction to Modal and Temporal Logics 6 December 2007 39 The Canonical Model Mr = (Wc, Rc, $c) Wc : = {X* | X* is a maximal-consistent extension of r} = 0 w Rc v iff {^ 1 G w} C v ^c(w'p) := { Í othe^se Claim: []p G w iff Vv G Wc.(wRcv =>* p G v) Proof right to left: Suppose Vv g Wc.(wRcv =>* p g v). Must show []p g w. i.e. Vv G Wc.({V> | []^ G w} C v =>* p G v) Let ^ := A| G w} i.e. Vv g Wc.(M/ g v =>* p g v) i.e. Vv g Wc.^ — p G v by Lemma 8(—). i.e. r h/ v|/ — p (else can choose p0 = \|/ — p for some v) i.e. r h [](v|/ — p) by (Nec) Note r h — p) — (QH/ — []p) by (Ax) Hence r h ([]v|/ — []p) by (MP) Hence ([]v|/ — []p) g w. Note, 0 h ((Q^o) A (D^i)) — D0/>o A (exercise) Hence {[]v|/, ([]v|/ — []p)} c w. Hence []p g w by (MP). Introduction to Modal and Temporal Logics 6 December 2007 40 Truth Lemma Lemma 9 For every p and every w e Wc/ #c(w,p) = t iff p e w. Proof: Pick any p, any w e W. Proceed by induction on length l of p. l = 0: So p = p is atomic. Then, #c(w,p) = t iff p e w by definition of #c. Ind. Hyp.: Lemma holds for all formulae with length l less than some n > 0 Ind. Step: Assume l = n and proceed by cases on main connective p = []^: We have #c(w, []^) = t iff Vv G Wc.(wRcv tfc(v,V) = t iff Vv G Wc.(wRcV =>* ^ G v) iff G w by Lemma 8([]). (by defn of valuations (by IH) Exercise: complete the proof Introduction to Modal and Temporal Logics 6 December 2007 41 Completeness Proof Corollary 1 (Wc, Rc, #c) lh r Proof: Since r is in every maximal-consistent set extending it, we must have r c w for all w e Wc. By Lemma 9, w lh r, hence (Wc, Rc, #c) lh r Proof of Completeness: if r H D then r = p Suppose r H p. Hence r Hi p. Construct the canonical model Mr = (Wc, Rc, #c). Consider any ordering of formulae where p is the first formula and let the associated maximal-consistent extension of r be X*. Since r Hi p we must have —p e X*. The set X* appears as some world w0 e Wc (say). Hence there exists at least one world where —p e w0. By Lemma 9 w0 ll—p i.e. Mr h D. By Corollary 1, we know Mr lh r. Since the canonical model is a Kripke model, we have r = d. (i.e. not VM e K.M lh r =>- M lh d) Completeness: By contraposition, if r = d then r H (p. Introduction to Modal and Temporal Logics 6 December 2007 42 Notes r - p iff r = p relies on the canonical frame (Wc, Rc) being a Kripke frame by its definition. (i.e. (Wc, Rc) e K) Later we shall see that the canonical model is not always sound for -: that is we can have p where r - p and Mr \f p (incomplete logics) Beware: some books (e.g. Goldblatt) use the notation r - p for our r -/ p because then the deduction theorem holds: r, p — ^ iff r -/ p — ^ Exercise: Prove it. For us, the syntactic counterparts of Lemma 4 and Lemma 5 are: Lemma 10 r h p — ^ implies r, p h ^ Lemma 11 r, p h ^ implies 3n.r h []0p A • • • A []np — ^ Introduction to Modal and Temporal Logics 6 December 2007 43 Lecture 3: Logic = Syntax and (Semantics or Calculus) r = p : semantic consequence in class of Kripke models K r V p : deducibility in Hilbert calculus K Soundness: if r V p then r = p Completeness: if r V p then Mr = p and Mr gK. K = {p | 0 = p} the validities of Kripke frames K K = {p | 0 V p} the theorems of Hilbert calculus K Theorem 1 K = K The presence of R makes modal logics non-truth-functional. But Kripke models put no conditions on R. So what happens if we put conditions on R ? Introduction to Modal and Temporal Logics 6 December 2007 44 Valid Shapes and Frame Conditions A binary relation R is reflexive if vw g W.wRw. A frame (W, R) or model (W, R, #) is reflexive if R is reflexive. The shape [](/? — ^ is called T. A frame (W, R) validates a shape iff it forces all instances of that shape. i.e. for all instances ^ of the shape and all valuations # we have (W, R, #) lh ^ Lemma 12 A frame (W, R) validates T iff R is reflexive. Intuition: the shape T captures or corresponds to reflexivity of R. Introduction to Modal and Temporal Logics 6 December 2007 45 Valid Shapes and Frame Conditions A relation R is reflexive if Vw g W.wRw. The shape []p — p is called T. Lemma 13 [Correspondence] A frame (W, R) validates T iff R is reflexive. Proof(i): Assume R is reflexive and (W, R) l/ []V — V for some []V — V. Exists model (W, R, #) and wo g W with wo lh []V and wo l/ V. v lh V for all v with woRv woRwo Hence, wo lh V. Contradiction Proof(ii): Assume (W, R) forces all instances of []p — p, and R not reflexive. Exists wo g W such that woRwo does not hold. For all w g W, let #(w, po) = t iff woRw. (we define #) #(v,po) = t for every v with woRv, and #(wo,po) = f since not woRwo. wo / []po and wo l/ po hence wo l/ []po — po But []po — po is an instance of T hence wo lh []po — po. Contradiction. Introduction to Modal and Temporal Logics 6 December 2007 46 Valid Shapes and Frame Conditions A frame (W, R) is reflexive if Vw e W.wRw. The shape []p — p is called T. A frame (W, R) validates T iff R is reflexive. This correspondence does not work for models! A model (W, R, #) validates T iff R is reflexive is false! Consider the reflexive model M where: W = {w0} and R = {(w0, w0)} and # is arbitrary. This model must validate T since (W, R) is reflexive. Now consider the model M7 where: W = {v0,vi} R7 = {(v0,vi), (vi,v0)} is: #/( p) = / t if ^(w0,p) = t v uVJ 1 f otherwise Exercise: model M7 also validates T. But M7 is not reflexive! Introduction to Modal and Temporal Logics 6 December 2007 47 Summary: The Logic of Reflexive Kripke Frames Let KT be the class of all reflexive Kripke frames. Let KT be the class of all reflexive Kripke models. Let KT = K + [] y — y (shape T) as an extra modal axiom. Define r |=KT y to mean VM e KT.M \h r =^ M \h y. Define r /KT y to mean there is a derivation of y from r in KT. Soundness: if r /KT y then r |=KT y Proof: all instances of T are valid in reflexive frames. Completeness: if r /KT y then Mr =KT y and Mr e KT Proof: if Mr validates (all instances of) T then Mr is reflexive. (sic!) i.e. T-instance — ^1 e w iff e w =>* ^1 e w by Lemma 8(—). Vw, v e W.w Rc v iff {V> | []^ e w} C v implies wRcw Introduction to Modal and Temporal Logics 6 December 2007 48 More Axiom and Frame Correspondences Name Axiom Frame Class Condition T []p - p Reflexive Vw £ W.wRw D []p - ()p Serial Vw £ W3v £ W.wRv 4 []p - [][]p Transitive Vu, v, w £ W.uRv&vRw == uRw 5 ()[]p - []p Euclidean Vu, v, w £ W.uRv&uRw == vRw B p - []()p Symmetric Vu, v £ W.uRv == vRu ()p - []p Weakly-Functional Vu, v, w £ W.uRv&uRw == v = w 2 ()[]p - []()P Weakly-Directed Vu,v,w £ W.uRv&uRw == zb £ W.vRx&wRx 3 ()p A()V - Weakly-Linear Vu,v,w £ W.uRv&uRw == ()(p A()V) vRw or wRv or w = v V()(()p A V) V()(p A V) Let KAxA2 • • • An = K + A1 + A2 +----+ An. (any Ajs from above) Theorem 2 r hKA!A2...An p iff r =KA1A2-An p Introduction to Modal and Temporal Logics 6 December 2007 49 Correspondence, Canonicity and Completeness Normal modal logic L is determined by class of Kripke frames C if: V(/?.£ lh (/? ^ hL (/?. Normal modal logic L is complete if determined by some class of Kripke frames. A normal modal logic is canonical if it is determined by its canonical frame. A Sahlqvist formula is a formula with a particular shape (too complicated to define here but see Blackburn, de Rijke and Venema) Theorem 3 Every Sahlqvist formula y> corresponds to some first-order condition on frames, which is effectively computable from y>. Theorem 4 If each axiom is a Sahlqvist formula, then the Hilbert logic KAXA2 • • • An is canonical, and is determined by a class of frames which is first-order definable. Theorem 5 Given a collection of Sahlqvist axioms A15 • , Ak, the logic KAX A2 • • • Ak is complete wrt the class of frames determined by A1 • • • Ak. Introduction to Modal and Temporal Logics 6 December 2007 50 Not All First-Order Conditions Are Captured By Shapes Theorem 6 (Chagrov) It is undecidable whether an arbitrary modal formula has a first-order correspondent. Question: Are there conditions on R not captured by any shape ? Yes: the following conditions cannot be captured by any shape: Irreflexivity: Vw e W. not wRw Anti-Symmetry: Vu, v e W.uRv&vRu u = v Asymmetry: Vu, v e W.uRv =>* not (vRu) See Goldblatt for details. Introduction to Modal and Temporal Logics 6 December 2007 51 Second-Order Aspects of Modal Logics All of these conditions are first-order definable so it looked like modal logic was just a fragment of first-order logic ... An R-chain is a sequence of distinct worlds w0RwiRw2 • • •. Name Shape R Condition G []([]p — p) — []p transitive and no infinite R-chains Grz []([](p — []p) — p) — []p reflexive, transitive and no infinite R-chains The condition "no infinite R-chains" is not first-order definable since "finiteness" is not first-order definable. It requires second-order logic, so propositional modal logic is a fragment of quantified second-order logic. The logic KG has an interesting interpretation where []p can be read as "p is provable in Peano Arithmetic". These logics are not Sahlqvist. Introduction to Modal and Temporal Logics 6 December 2007 52 Shapes Not Captured By Any Kripke Frame Class Consider logic KH where H is the axiom schema []([]p p) — []p. Theorem 7 (Boolos and Sambin) The logic KH is not determined by any class of Kripke frames. G Boolos and G Sambin. An Incomplete System of Modal Logic, Journal of Philosophical Logic, 14:351-358, 1985. Incompleteness first found in modal logic by S KThomason in 1972. Beware, there is also a R H Thomason in modal logic literature. Can regain a general frame correspondence by using general frames instead of Kripke frames: see Kracht. Kracht shows how to compute modal Sahlqvist formulae from first-order formulae. SCAN Algorithm of Dov Gabbay and Hans Juergen Ohlbach automatically computes first-order equivalents via the web. Introduction to Modal and Temporal Logics 6 December 2007 53 Sub-Normal Mono-Modal Logics Hilbert Calculus S = PC plus modal axioms (not K) (Id) r /s y ye r (Ax) r /s y y is an instance of an axiom schema (MP) r \-s cp r hg cp —> ip (Mon) r /s []y — []^ r /s y — v> no rule (Nec) r -s y : iff there is a derivation of y from r in S. Such modal logics are called "sub-normal". r _s y: needs Kripke models (W, Q, R, #) where: W is a set of"normal" worlds and # behaves as usual, and Q is a set of"queer" or "non-normal" worlds where #(wg, ()y ) _ t for all y and all wg e Q by definition. Then (Nec) fails since M \h y ^ M \h []y i.e. every non-normal world makes []y false. Applications in logics for agents: _ y =>* _ []y says that "if y is valid, then y is known", but agents may not be omniscient, hence want to go sub-normal". Introduction to Modal and Temporal Logics 6 December 2007 54 Regaining Expressive Power Via Nominals Atomic Formulae: p :: = p0 I Pi I P2 | • • • (Atm) Nominals: i ::= i0 I ii I i2 I • • • (Nom) Formulae: p ::= p I i I —p I ()p I []p I p A p I p V p I p —► p (Fml) Valuation: for every i, #(w, i) = t at only one world Intuition: i is the name of w Expressive Power: Irreflexivity: Vw g W. not wRw i —► — ()i Anti-Symmetry: Vu, v g W.uRv=>* u = v i —► —► i) Asymmetry: Vu, v g W.uRv =>* not (vRu) i —► — And many more see: Blackburn P. Nominal Tense Logics, Notre Dame Journal Of Formal Logic, 14:56-83, 1993. Introduction to Modal and Temporal Logics 6 December 2007 55 Lecture 4: Tableaux Calculi and Decidability Motivation: Finding derivations in Hilbert Calculi is cumbersome: r,p h iff r h p — fails! r,p h iff r h ([]0p a []ip• []np) — ? ? ? - £ - £ (p ) - p -(MP) -(Nec) - p ^ - []p Resolution: one rule suffices for classical first-order logic, but not so for modal resolution Decidability: questions can be answered via refinements of canonical models called filtrations, but there are better ways ... For filtrations see Goldblatt. Introduction to Modal and Temporal Logics 6 December 2007 56 Negated Normal Form NNF: A formula is in negation normal form iff all occurrences of - appear in front of atomic formulae only, and there are no occurrences of —. Lemma 14 Every formula p can be rewritten into a formula p7 such that p7 is in negation normal form, the length of p7 is at most polynomially longer than the length of p, and 0 = p p7. Proof: Repeatedly distribute negation over subformulae using the following valid principles: = —(p A ?/>) (—p V —^) |= —(p V ?/>) (—p A —^) |= p p = —()p []—p Introduction to Modal and Temporal Logics 6 December 2007 57 Examples: NNF Example: -([](p0 — pi) — ([]p0 — []pi)) [](p0 — pi) A -([]p0 — []pi) [](p0 — pi) A ([]p0 A-[]pi) [](-p0 V pi) A ([]p0 A()-pi) Example: -([]p0 — p0) ([]p0) A (-p0) -([]p0 — [][]p0) ([]p0) A (-[][]p0) ([]p0) A (()-[]p0) ([]p0) A (()()-p0) Introduction to Modal and Temporal Logics 6 December 2007 58 Tableau Calculi for Normal Modal Logics Static Rules: (id) p; — p; X x (A) (V) X | 0; X v V 0; X Transitional Rule: (()K) tp;x V0.[]0 0 Z []X = {[]0|0 0 X} X, Y, Z are possibly empty multisets of formulae and p; X stands for {p} multiset-union X so number of occurences matter A K-tableau for Y is an inverted tree of nodes with: 1. a root node nnf Y 2. and such that all children nodes are obtained from their parent node by instantiating a rule of inference A K-tableau is closed (derivation) if all leaves are (id) instances, else it is open. Introduction to Modal and Temporal Logics 6 December 2007 59 Rules: (Name) MSet if numerator is K-satisfiable MSeti | MSetn then some denominator is K-satisfiable Examples of K-Tableau -([](p0 — p1) — ([]p0 — --------------------------------------(nnf ) [](-P0 V P1)A([]p0 A()-P1) -(A) [](-P0 V([]P0A()-P1) -(A) -w- ^ -(v) -p0; p0; -p1 I p1; p0; -p1 X X There is a closed K-tableau for -([](p0 — p1) — ([]p0 — Introduction to Modal and Temporal Logics 6 December 2007 60 Examples of Tableau -(Dpo-DDpo) -([]P0 - PO) ([]po)A(()()^o) ^ ([]po) A (A) []Po;0 0. Ind. Step: Then nnf Y has a closed K-tableau of length k. Top-most rule? (()K): So the top-most rule application is an instance of the (()K)-rule. p; X has closed K-tableau By IH. p; X is not K-satisfiable. Lemma 22: if ()p; []X; Z is K-satisfiable then p; X is K-satisfiable. Hence Y = (()p; []X; Z) cannot be K-satisfiable. Corollary 2 If {-p} has a closed K-tableau then 0 = p Introduction to Modal and Temporal Logics 6 December 2007 64 Downward Saturated Or Hintikka Sets A set Y is downward-saturated or an Hintikka set iff: y e Y ye Y a: yA V e Y =>* ye Y and V e Y v: yv V e Y =>* ye Y or V e Y —: y — V e Y =>* ye Y or V e Y Downward-saturated set is consistent if it does not contain {y, -y}, for any y. Don't need maximality: it is not demanded that Vy .y e Y or - ye Y. (Hintikka) Introduction to Modal and Temporal Logics 6 December 2007 65 Model Graphs A K-model-graph for set Y is a pair (W, <) where W is a non-empty set of downward-saturated and consistent sets, some w0 e W contains Y, and < is a binary relation over W such that for all w: (): ()p e w =>* (3v e W.w < v & p e v) []: []p e w =>* (Vv e W.w < v =>* p e v). Lemma 23 (Hintikka) If there is a K-model-graph (W, <) for set Y then Y is K-satisfiable. Proof: Let (W, R, #) be the model where R = < and tf(w,p) = t iff p e w. By induction on the length of a formula p, show that tf(w, p) = t iff p e w. Since Y C w0 we have w0 lh Y. Introduction to Modal and Temporal Logics 6 December 2007 66 Creating Downward-Saturated and Consistent Sets Lemma 24 If every K-tableau for Y is open, then Y can be extended into a downward-saturated and consistent Y* so every K-tableau for Y* is also open. Proof: Suppose no K-tableau for Y closes. Now consider the following systematically constructed K-tableau. Stage 0: Let w0 = Y. Stage 1: Apply static rules giving finite open branch of nodes w0, w1? • • • , wk. Let Y* be the multiset-union of w0, • • • , wk. Claim: Y* is downward-saturated (obvious) and consistent, and Y C Y*. By Contraction Lemma 18, we know (/?; X has (no) closed K-tableau iff (/?; (/?; X has (no) closed K-tableau. (adding copies cannot affect closure) Tableau for Y* cannot close since construction of Y* just adds back the principal formulae of each static rule application. can treat Y* as a set! Introduction to Modal and Temporal Logics 6 December 2007 67 Completeness and Decidability Lemma 25 If no K-tableau for Y is closed, there is a K-model-graph for Y. Proof: Suppose no K-tableau for Y closes. Now consider the following systematic procedure Stage 0: Let w = Y. Stage 1: Apply static rules giving downward-saturated and consistent node w* (Lemma 24) Stage 2: Let , , • • • ()pn be all the ()-formulae in the current node. So the current node looks like: Op^; []X; Zi for each i =1 • • • n. Repeat Stages 1 and 2 on each node vi = (pi; X), and so on ad infinitum. Each (())-rule application reduces maximal-modal degree, giving termination. For each i =1 • • • n apply: (()) Vi\X * <— w* <— vi Let W be set of all *-nodes, let w* < v* i (W, <) is a K-model-graph for Y Introduction to Modal and Temporal Logics 6 December 2007 68 Decidability and Analytic Superformula Property Subformula property: the nodes (sets) of a K-tableau for Y (i.e. nnf Y) only contain formulae from nnf Y. Subformula property will hold if all rules simply break down formulae or copy formulae across. Analytic superformula property: the nodes (sets) of a L-tableau for Y (i.e. nnf Y) only contain formulae from a finite set Y7 computable from nnf Y (but possibly larger than nnf Y). Analytic superformula property will hold if all rules that build up formulae cannot be applied ad infinitum. The main skill in tableau calculi is to invent rules with the subformula property or the analytic superformula property! Introduction to Modal and Temporal Logics 6 December 2007 69 Completeness W.R.T. K-Satisfiability Theorem 9 If there is no closed K-tableau for Y then Y is K-satisfiable. Proof: Suppose every K-tableau for Y is open. Use Lemma 25 to construct a K-model-graph (W, <) for Y. For all w e W, let p) = t iff p e w. Then (W, <, ^) contains a world w0 with w0 = Y by Hintikka's Lemma 23. Corollary 3 If there is no closed K-tableau for {-p} then = p. Corollary 4 There is a closed K-tableau for Y iff Y is not K-satisfiable. Corollary 5 There is a closed K-tableau for {-p} iff p is K-valid. Introduction to Modal and Temporal Logics 6 December 2007 70 What About Logical Consequence: a concrete example Write r hr y : iff there is a closed K-tableau for (r; - y) i.e. nnf (r; -y) Want Completeness: r t/r y 3M.M \h r & M \/ y Consider: r :_ {p0} and y :_ . Then nnf (r; - y) has only one (open) K-tableau: (H-y) -(nnf ) (p0; -«-(0) wo _ {P0, } wi _ {-pi} woRwi Problem: although w0 \h r, we don't have w1 \h r. So M \f y but M \f r. If only we could make w1 force r too ... Introduction to Modal and Temporal Logics 6 December 2007 71 Regaining Completeness WRT Logical Consequence Change (()) rule from (()) ih^MiZ 0 Z to: p; x Transitional Rule: (()r) W ' ' V^.[]^ 0 ^ (R-successor forces l~) p; X;nnf r Semantic reading: if numerator is L-satisfiable in a model that forces r - (new) then some denominator is L-satisfiable in a model that forces r Stage 2: For each i = 1 • • • n apply: By completeness: r HT p : iff (3M.3w.M lh r &w lh (r; -p)) iff lh r & M l/ p) iff r = p But there is a slight problem ... (TINSTAAFL) Introduction to Modal and Temporal Logics 6 December 2007 72 Regaining Decidability Problem: K-tableau can now loop for ever: r := {()p0}, and

) -------------(nnf ) (()p0; -(on (p0; ()p0) -(on (p0; ()p0) —77.— (on Solution: if we ever see a repeated node, just add a <-edge back to previous copy on path from current node to root. Introduction to Modal and Temporal Logics 6 December 2007 73 Other Normal Modal Logics KT: Static Rules: (id), (a), (v), plus (t) —yrf'* v \\u> unstarred Transitional Rule: (()r) Z V^-DV' 0 ^ (unstarall Q-formulae) (/?; x;nnf r K4: Static Rules: (id), (A), (v) Transitional Rule: «>r4) ^\^X\rtL V 0 Z KT4: Static Rules: (id), (A), (v), (t) Transitional Rule: (()I~T4) ^ *A W?.[]^ 0 Z (unstarall []-formulae) ( ; [] x ; nnf r Introduction to Modal and Temporal Logics 6 December 2007 74 Examples of KT-Tableau KT: Static Rules: (id), (a), (v), plus (T) —v Wf unstarred p; ([]p) ; X Transitional Rule: «}r~) *' ^ V4>.[]ip 0 Z (unstarall Q-formulae) p; X;nnf r — ([]p0 — p0) ----------------nnf ([]p0) A —p0 -(a) ([]p0); —p0 -(T) p0, ([]p0)*; —p0 X There is a closed KT-tableau for —([]p0 — p0) i.e. 0 -KT []p0 — p0 Starring stops infinite sequence of T-rule applications. Introduction to Modal and Temporal Logics 6 December 2007 75 Examples of K4-Tableau K4: Static Rules: (id), (a), (v) Transitional Rule: «>r4) ^f W>.[]V £ Z -([]p0 — [][]p0) ---------------------nnf ([]p0) a (()()-p0) -(a) []p0; ()()-p0 /n x ()p0;[]()p0 —-—-—(0r4) -((>r4) p0;[]p0; 0-pT4) {)(p] []f*; Z V^W 0 Z All depends upon: Lemma : if ()y; []X; Z is KT4-satisfiable then y; X is KT4-satisfiable. Proof: Suppose ()y; []X; Z is is KT 4-satisfiable. i.e. exists transitive Kripke model (W, R, #) and some w e W with w lh ()y;[]X; Z i.e. exists transitive Kripke model (W, R, #) and some v e W with wRv and v lh (y; X;[]X) ([]X — [][]X) i.e. exists transitive Kripke model (W, R, #) and some v e W with wRv and v h (y; []X) can regain X by T rule Introduction to Modal and Temporal Logics 6 December 2007 78 Tableaux Versus Hilbert Calculi Algorithm: Systematic procedure gives algorithm for finding (closed) tableaux. Decidability: easier than in Hilbert Calculi. Modularity: Must invent new rules for new axioms. Reuse completeness proof based upon systematic procedure with tweaks. Rules require careful design to regain decidability e.g. starring, looping, dynamic looping etc. Automated Deduction: Logics WorkBench http: //www.lwb.unibe.ch has implementation of tableau theorem provers for many fixed logics e.g. K, KT, K4, KT4, ... Automated Deduction: The Tableaux WorkBench http: //arp. anu. edu. au/~abate/twb provides a way to implement tableau theorem provers for any tableau calculus that fits its syntax e.g. KD45, KtS4, Int, IntS4, ... Introduction to Modal and Temporal Logics 6 December 2007 79 Lecture 5: Tense and Temporal Logics Tense Logics: interpret []p as "p is true always in the future". W represents moments of time R captures the flow of time Temporal Logics: similar, but use a more expressive binary modality pU^ to capture "p is true at all time points from now until i/j becomes true". Shall look at Syntax, Semantics, Hilbert and Tableau Calculi. Introduction to Modal and Temporal Logics 6 December 2007 80 Tense Logics: Syntax and Semantics Atomic Formulae: p :: = pq \ pi \ p2 \ ••• Formulae: p ::= p \—p \ (F)p \ [F](p \ (P)p \ [P]p \ p A (p \ (p V (p \ (p — (p Boolean connectives interpreted as for modal logic. Given some Kripke model (W, R, &) and some w e W, we compute the truth value of a non-atomic formula by recursion on its shape: a/ /ea \ _ / t if tf(v,p)= t at some v e W with wRv ů(w, [P]) = t at some v e W with vRw if tf(v, y>) = t at every v e W with vRw if tf(v, y>) = t at every v e W with wRv Introduction to Modal and Temporal Logics 6 December 2007 81 Tense Logics: Syntax and Semantics 0(w, (F)p) t if #(v, p) = t at some v e W with wRv f otherwise t if #(v, p) = t at every v e W with wRv f otherwise t if #(v, p) = t at some v e W with vRw f otherwise t if #(v, p) = t at every v e W with vRw f otherwise Example: If W = {w0, } and R = {(w0, wi), (w0, w2)} and ,p3) = t then (W, R, #) is a Kripke model as pictured below: wo W2 #(w0, (F)p3) #(wo, [P]pi) = t = t = t Introduction to Modal and Temporal Logics 6 December 2007 82 Hilbert Calculus for Modal Logic Kt Axiom Schemata: Axioms for PC plus: K[F]: [F](p — V) — ([F]p — [F]V) K[P]: [P](p — V) — ([P]p — [P]V) FP: p — [F](P)p PF: p — [P](F)p Rules of Inference: (Ax) —— cp is an instance of an axiom schema r h p (id) r— v€ r (MP) rh^rhrhf ^ (Nec[F]) J"^ (Nec[P]) r^f^- Soundness, Completeness, Correspondence etc. : Let Kt = K be class of all Kripke Tense frames r HKtA1?A2,...,An p iff r =KtA1,A2,...,An p Introduction to Modal and Temporal Logics 6 December 2007 83 Different Models of Time Arbitrary Time: Kt Reflexive Time: p — (F)p Transitive Time: (F)(F)p — (F)p Dense Time: (F)p — (F)(F)p Never Ending Time: [F]p — (F)p Backward Linear: (F)(P)p — (P)p v p v (F)p Forward Linear: (P)(F)p — (F)p v p v (P)p Tableau Calculi also exist but require even more complex loop detection often called "dynamic blocking". Discrete (Z, <) , Rational (Q, <), Real (R, <) linear and non-reflexive models of time also possible: see Goldblatt. Tableau-like calculi exist: see Mosaic Method Introduction to Modal and Temporal Logics 6 December 2007 84 PLTL: Propositional Linear Temporal Logic Atomic Formulae: p :: = p0 | Pi | P2 | • • • Formulae: p ::= p | -p | + p | [F]p | (F )p | p | p A p | p V p | p — p Boolean connectives interpreted as for modal logic. Linear Time Kripke Model: (S, a, R, #) S: non-empty set of states a: N — S enumerates S as sequence a0• • • with repetitions when S finite S x Atm — {t, f} R: is a binary relation over S Condition: R = a * (R is the reflexive and transitive closure of a) Introduction to Modal and Temporal Logics 6 December 2007 85 Semantics of PLTL +p) 1 f otherwise (f)p) = jt if ^(si'p) = t forsome j > i u x 1 f otherwise [F]p) = U ift|h(sw,ip) = t fora» j > i i f otherwise p u^) = ft if 3k > )= t & Vj.i < j i otherwise [F]y) _ t f if ^(sj, y ) _ t for all j > i otherwise t f if 3k > i.tf(sk,V) _ t & Vj.i otherwise < j < k ^(sj, y) _ t si+1 • • • Sj • • • s k -(p U q),-q ... -q ^ ^ ^ - q q is always false, or -(p U q) ^ ^ ^ -p, -q ^ ^ ^ q p false before q true Note: when k _ i, the state sk is the first state after si where q is true. And p is false in some sj before state sk. Introduction to Modal and Temporal Logics 6 December 2007 87 Hilbert Calculus for PLTL Axiom Schemata: axioms for PC plus K[F]: [F](p — V) — ([F]p — [F]V) K©: ©(p — V) — (©p — ©V) Fun: + -p -m. -©p Mix: [F]p — (p A ©[F]p) Ind: [F](p — + p) — (p — [F]p) Ui: (pUV) — (F)V U2: (pUV) V V (-V A p A +(pUV)) Rules: (Id), (Ax), MP and (Nec[F]) and (Nec+) Introduction to Modal and Temporal Logics 6 December 2007 88 Tableau Calculus for PLTL Presence of Induction Axiom Ind means no Unitary cut-free sequent calculus (must guess induction hypothesis) Cannot just "jump" on (F)p because of its interaction with + which demands "single steps" Requires a two pass method: build a model-graph, check that it is contains a model. Introduction to Modal and Temporal Logics 6 December 2007 89 Tableau Calculus for PLTL: Pass 1 Stage 0: put w0 = Y Stage 1: repeatedly apply usual (a) and (v) rules together with the following to obtain a downward-saturated node w0 in which each non-atomic formula is marked as "done" or is of the form ©(/?: -0y> — 0-y> [F]y> — (y> a ©[F]y>) (F)y> — (y> v 0(F)y>) (y>) — V v a y> a ©(y>)) Stage 2: Current node is now of the form ©X; Z where Z contains only atoms, negated atoms, and "done" formulae. Create a ©-successor w1 containing X. Stage 3: Saturate w1 via Stage 1 to get w1 and add w0R©w1 if w1 is new, else add w0R©v* for the node v* which already replicates Stage 4: If w1 is new then repeat and so on until no new *-nodes turn up giving a possibly cyclic graph. Introduction to Modal and Temporal Logics 6 December 2007 90 Tableau Method for PLTL: Pass 2 An eventuality is a formula (F)p or pU^ A path is a maximal (cyclic) sequence of nodes starting at the root. "Maximal" means "cannot avoid repetition" (unwind) A path fulfills (F)p if some node on it contains p A path fulfills p UV> if some node on it contains ^ and between nodes contain p Delete all nodes that contain a pair {p, -p}. Repeatedly delete all nodes who now do not have an + -successor. If some single path fulfills all eventualities contained in its nodes then Y is PLTL-satisfiable, otherwise it is not. Note: all eventualities on that path must be fulfilled on that path! Introduction to Modal and Temporal Logics 6 December 2007 91 Lecture 6: Fix-point Logics PLTL: linear time temporal logic CTL: computation tree logic PDL: propositional dynamic logic LCK: logic of common knowledge Look at CTL but using only one relation R rather than R _ a* Introduction to Modal and Temporal Logics 6 December 2007 92 CTL: Computation Tree Logic Atomic Formulae: p :: = po | p1 | p2 | • • • (AP) Formulae: p ::= p | -p | p A p | p V p | p — p |EXp|AXp | E(pUV) | A(pUV) | E(pB V) | A(pB V) (Fml) Note: Ep is not a formula! Unary Modal connectives are: EX• and AX• Binary Modal Connectives are: E(• U •) A( U •) A(-B •) E(• B •) NNF: we shall later assume that all formulae are in Negation Normal Form Introduction to Modal and Temporal Logics 6 December 2007 93 Semantics of CTL Transition Frame: is a pair (W, R) where W is a non-empty set of worlds and R is a binary relation over W that is total (Vw e W. 3v