index.md (5248B)
1 +++ 2 title = 'Semantics: truth and validity, game semantics for formula validity' 3 template = 'page-math.html' 4 +++ 5 # Semantics: truth and validity, game semantics for formula validity 6 ## Game semantics 7 This is an approach to determine if a formula φ holds in a pointed model M, w. 8 9 We have: 10 - model M = ((W,R), V), world w ∈ W, formula φ 11 - two players: 12 - Verifier V claims that φ is true in w (sort of like ∀) 13 - Falsifier F claims that φ is false in w (sort of like ∃, try to find a _witness_) 14 - position: pair (w, φ) with w ∈ W a world and φ a formula 15 - move: from position (w, φ), determined by main operator of φ 16 17 Assume that negation only applied to prop. variables. 18 Transform formulas from ¬ □ p to ◇ ¬ p, ¬(p ∧ q) to ¬p ∨ ¬q. 19 20 The position determines the move, e.g. in a position (t, ◇ φ), V chooses a successor _u_ of _t_, and play continues with (u, φ). 21 For (t,p), if p is true in t then V wins, otherwise F wins. 22 For (t, ¬p), if p is false in t then V wins, otherwise F wins. 23 If a player should but cannot choose a successor, they lose. 24 25 Who starts: 26 - V: ∨, ◇ 27 - F: ∧, □ 28 29 A complete game tree for φ and (M,w) starts with (w,φ) and contains all possible moves. 30 A strategy for player P is subset of steps for P, and it's a winning strategy if it ensures that P wins the game. 31 32 To determine validity: φ is true in M in s ⇔ V has a winning strategy for M,s,φ. 33 34 <details> 35 <summary>Example: complete game tree</summary> 36 37 Diagram: 38 39  40 41 <details> 42 <summary>Graphviz code</summary> 43 44 <!-- :Tangle(dot) states.dot --> 45 ```dot 46 digraph states { 47 1 -> 2 48 1 -> 3 49 2 -> 3 50 3 -> 2 51 3 -> 4 52 4 -> 2 53 4 -> 3 54 } 55 ``` 56 57 </details> 58 59 Given: 60 - question: formula ◇ p ∨ □ ◇ p, is it valid in state 2? 61 - p is true in state 3. 62 63 Complete game tree: 64 65  66 67 <details> 68 <summary>Graphviz code</summary> 69 70 <!-- :Tangle(dot) tree.dot --> 71 ```dot 72 digraph gametree { 73 top [label="[V] ◇ p ∨ □ ◇ p, 2"] 74 l11 [label="[V] ◇ p, 2"] 75 l12 [label="[F] □ ◇ p, 2"] 76 top -> l11 77 top -> l12 78 l21 [label="p 3"] 79 l22 [label="[V] ◇ p, 3"] 80 l11 -> l21 81 l12 -> l22 82 l31 [label="Verifier wins"] 83 l32 [label="p, 2"] 84 l33 [label="p, 4"] 85 l21 -> l31 86 l22 -> l32 87 l22 -> l33 88 l41 [label="Falsifier wins."] 89 l42 [label="Falsifier wins."] 90 l32 -> l41 91 l33 -> l42 92 } 93 ``` 94 95 </details> 96 </details> 97 98 ## Truth and validity 99 There are different levels of validity: 100 - (((W,R),V),w) ⊨ φ means φ is valid in a state/world w. 101 - (W,R) ⊨ φ means φ is valid in a frame (W,R). 102 - ⊨ φ means φ is valid universally (a tautology). 103 104 If a part is omitted, it's implicitly universally quantified. 105 106 Satisfiability: 107 - φ _satisfiable in model M_ if there's a world w ∈ M such that M,w ⊨ φ 108 - φ _satisfiable_ if there's a model M and a world w ∈ M such that M,w ⊨ φ 109 - φ valid iff ¬ φ not satisfiable 110 111 φ and ψ _semantically equivalent_ if they're only valid in the same worlds, i.e. ∀ M,w: M,w ⊨ φ ⇔ M,w ⊨ ψ 112 113 <details> 114 <summary>Example: showing universal validity</summary> 115 116 Show universal validity of □ (φ → ψ) → (□ φ → □ ψ) 117 118 1. let F = (W,R) be frame, V valuation on F, let x ∈ W. 119 2. Assume a1: F,V,x ⊨ □ (φ → ψ) 120 3. Assume a2: F,V,x ⊨ □ φ 121 4. Aim to show F,V,x ⊨ □ ψ. 122 5. □ is universal quantification, so take an arbitrary successor y ∈ W. 123 6. If Rxy, aim to show y ⊨ ψ. If not, □ ψ holds. 124 7. Have y ⊨ φ → ψ and y ⊨ φ. 125 8. From a2, have y ⊨ φ. 126 9. From a1, have have y ⊨ ψ. 127 10. Hence x ⊨ □ ψ, hence x ⊨ □ φ → □ ψ. Hence formula is valid. 128 129 </details> 130 131 ## Preservation of truth and validity 132 ### Substitution 133 Substitution for propositional variables 134 - σ : Var → Form 135 - T and ⊥ not substituted 136 137 If (W,R), V ⊨ φ then not necessarily $(W,R), V \models \phi^{\sigma}$ 138 139 But validity in a _frame_ is preserved under substitution: if F ⊨ φ, then $F \models \phi^{\sigma}$ for any substitution σ. 140 141 ### Alternative semantics 142 The interpretation $[\\![ \phi ]\\!] _{M}$ of a formula φ in model M = (W,R,V) is set of worlds in which φ is true. 143 144 M, w ⊨ φ iff $w \in [\\![\phi]\\!]_{M}$ 145 146 M ⊨ φ iff $[\\![\phi]\\!]_{M} = W$ 147 148 ### Preservation of truth and validity 149 Local truth preserved by modus ponens: if M, w ⊨ φ → ψ and M, w ⊨ φ then M, w ⊨ ψ 150 151 Global truth preserved by modus ponens and necessitation: if M ⊨ φ then M ⊨ □ φ 152 153 Frame validity preserved by modus ponens, necessitation, and substitution: if F ⊨ φ then $F \models \phi^{\sigma}$. 154 155 ## Modal tautologies 156 - ⊨ □ (p → q) → □ p → □ q 157 - If ⊨ φ → ψ and ⊨ φ then ⊨ ψ 158 - If ⊨ φ then ⊨ □ φ 159 - If ⊨ φ then $\models \phi^{\sigma}$ 160 161 ## Characterizations of frame properties 162 If F reflexive then F ⊨ □ p → p. 163 This holds in the opposite. 164 So the formula □ p → p characterizes the frame property 'reflexivity'. 165 166 In general, "formula φ characterizes the frame property P" means: F has property P iff F ⊨ φ. 167 If you need to prove that a formula characterizes a property, you need to prove this bi-implication in _both_ directions. 168 169 ## Modal equivalence 170 Two states M, w and M', w' are modally equivalent if they satisfy the same formulas.