index.md (3540B)
1 +++ 2 title = 'Intro to Modal Logic (operators, frames, models, tautologies)' 3 +++ 4 5 # Intro to Modal Logic (operators, frames, models, tautologies) 6 ## First-order propositional logic 7 Includes variables, T, ⊥, not, and, or, implication. 8 Proofs are given by structural induction. 9 Precedence is ¬, then ∧∨, then →. 10 11 a valuation v : Var → {0,1} maps propositional variables to truth values. 12 i.e., it tells you what variables are true. 13 14 the semantics of a formula under a valuation is defined with ⟦p⟧ᵥ = v(p), with p ∈ Var 15 16 if ⟦φ⟧ᵥ = 1 (i.e. φ is true in v), we write v ⊨ φ (read "v models φ"). 17 - then also: φ has a model, namely the model with state _v_, so φ is _satisfiable_ 18 19 If every model of all φᵢ is a model of ψ, we write φ₁,...,φn ⊨ ψ 20 - then ψ is a semantic consequence of φ₁,...,φn 21 22 If v ⊨ φ for all valuations of v, then universally ⊨ φ (φ is a tautology) 23 24 Soundness: ⊢ implies ⊨ ("what we can derive is true"). proved by induction on length of proof 25 26 Completeness: ⊨ implies ⊢ ("what is true can be derived"). can be proven using consistency 27 28 ## Basic modal logic 29 Basic model logic operators: 30 - □: necessary, known, provable 31 - ◇: possible, considered possible 32 33 In a diagram, one of these symbols is exactly one transition step (use multiple for multiple steps). 34 35 - ◇ φ ⇔ ¬□ ¬φ 36 - □ φ ⇔ ¬◇ ¬φ 37 38 Examples in natural language: 39 - "whatever is necessary is possible" == □φ → ◇φ 40 - □ can also mean "I know", e.g. "I know that someone appreciates me" == ∃x.□A(x, M) 41 42 Loeb's formula: □ (□ p → p) → □ p 43 44 Veridicality: □ φ → φ 45 46 Truth is relative to current situation/world/environment: 47 - formulas evaluated in given structure (i.e. world, model, frame, or universally) 48 - necessity (□): truth in all accessible worlds. if there are no accessible worlds, it's true. 49 - □ T: holds always 50 - □ ⊥: holds in blind states (those without a successor) 51 - possibility (◇): truth in some accessible world (at least one). if there are no accessible worlds, it's false. 52 - ◇ ⊥: never holds (can never do a step to a state where ⊥ holds) 53 - ◇ T: holds in states with a successor 54 55 Dualities: 56 - ◇ φ ≡ ¬ □ ¬ φ 57 - □ φ ≡ ¬ ◇ ¬ φ 58 59 ## Frames 60 A situation is set by a frame F = (W,R) 61 - W ≠ ∅ set of possible worlds/states 62 - R ⊆ W × W an accessibility/transition relation 63 64 A frame is just the states and transitions between them, without a valuation (i.e. without saying what's true in each state). 65 66 A frame could be (ℕ, <), or ({1,2,3,4}, {(1,2), (2,4), (1,3), (3,4), (2,2)}) 67 68 ## Models 69 model: pair M = (F, V) 70 - a frame F = (W,R) 71 - a valuation V : Var → W → {0,1}, or V : Var → P(W) 72 - the valuation says which letters/formulas are true in which states 73 - possible notation: 74 - V : Var → P(W) means Var → W → {0,1} 75 - V(p,w) = 1 is the same as w ∈ V(p) 76 77 78 pointed model: pair (M,w) of model M and w a world in M (i.e. you zoom in to a specific state in M) 79 80  81 82 83 ## Distinguishing and characterizing states 84 A formula φ _characterizes_ a state x in model M if φ is true in x but not in other states of M. 85 86 A formula φ _distinguishes_ state x from state y in a model M if φ is true in x but not in y. 87 88 <details> 89 <summary>Example</summary> 90 91  92 93 Above: 94 - the formula 3 ⊨ □ ⊥ characterizes state 3 95 - the formula 2 ⊨ ◇ □ ⊥ characterizes state 2 96 97 </details>