modal-logic.wiki (2066B)
1 %template math 2 == Modal logic == 3 modal logic allows reasoning about dynamics -- futures, knowledge, beliefs, etc. 4 5 modalities (unary connectives): 6 * □ (box): sure, always, has to be, knows, guaranteed (kinda like ∀) 7 * ◇ (diamond): possibly, sometimes, maybe, believes is possible, possible result (kinda like ∃) 8 9 Kripke model `M = (W, R, L)` consists of: 10 * W worlds 11 * R accessibility relation 12 * L labeling function: which propositional letters are true in which world (`w ⊩ p ↔ p ∈ L(w)`) 13 14 Kripke models define truth _per world_. 15 16 {{local:../img/kripke-model-and-graph.png|Kripke model and graph}} 17 18 === Truth in worlds === 19 `M, w ⊩ Φ` means formula Φ is true in world w of Kripke model M. 20 21 ◇ Φ is true in world w if there exists a world w' such that R(w, w') and Φ is true in w'. 22 23 □ Φ is true in world w if Φ is true in all worlds w' with R(w, w'). special case when world has no outgoing edge, ◇ Φ never holds and □ Φ always holds. 24 25 === Truth in Kripke models === 26 Φ is true in Kripke model `M = (W, R, L)` (i.e. M ⊨ Φ), iff x ⊩ Φ for every world x ∈ W. 27 28 all propositional tautologies also hold in modal logic. 29 30 === Semantic implication/entailment === 31 M,w ⊨ ψ in every world w in every Kripke model where M,w ⊨ Φ₁, ..., M,w ⊨ Φn. 32 33 modal validity: ⊨ ψ if in every world w in ever Kripke model M holds M,w ⊨ ψ. 34 35 modal logical equivalence: `Φ ≡ ψ` if `M,w ⊨ Φ ↔ M,w ⊨ ψ`. in other words, Φ ≡ ψ ↔ Φ ⊨ ψ and ψ ⊨ Φ. 36 37 === Frames === 38 frame: Kripke model without labeling. `F = (W,R)`, W worlds, R accessibility relation 39 40 Φ is valid in frame F (i.e. F ⊨ Φ) if for _every_ labeling L, Kripke model M = (W,R,L) makes Φ true. 41 42 Correspondence of formulas and frame properties 43 * reflexive: 44 * F ⊨ □ p → p 45 * F ⊨ p → ◇ p 46 * symmetric: 47 * F ⊨ q → □ ◇ q 48 * F ⊨ ◇ □ p → p 49 * transitive: 50 * F ⊨ □ p → □ □ p 51 * F ⊨ ◇ ◇ p → ◇ p 52 * serial: 53 * F ⊨ ◇ T 54 * F ⊨ □ p → ◇ p 55 * functional: □ p ↔ ◇ p 56