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