index.md (3515B)
1 +++ 2 title = 'Exercise class 1' 3 +++ 4 # Exercise class 1 5 ## Universal validity examples 6 - □ φ → ◇ φ 7 8 Not universally valid, see model with one point & no relations. 9 Has □ p but not ◇ p. 10 11 - ◇ φ → □ φ 12 13 Not universally valid. 14 15 Counterexample: 16 - W = {1,2}. R = {(1,1), (1,2)}. V(p) = {1}. 17 - Show ◇ p → □ p. 18 - (W,R),V,1 ⊨ ◇ p because R11 and 1 ⊨ p. 19 - But 1 ⊭ □ p because R12 and 2 ⊭ p. 20 - So not universally valid. 21 22 - □ p → □ □ p 23 24 No. 25 Counterexample when left side of implication holds but right does not: 26 27  28 29 <details> 30 <summary>Dot code</summary> 31 32 ```dot 33 digraph g { 34 rankdir="LR" 35 2 [label="2", xlabel="p"] 36 1 -> 2 37 2 -> 3 38 } 39 ``` 40 41 </details> 42 43 - ¬ □ p → □ ¬ □ p 44 45 No. 46 Counterexample: 47 48  49 50 <details> 51 <summary>Dot code</summary> 52 53 ```dot 54 digraph g { 55 rankdir="LR" 56 3 [label="3", xlabel="p"] 57 1 -> 2 58 2 -> 3 59 } 60 ``` 61 62 </details> 63 64 ## 1 65 ### 1a 66 W = {a₁...a₇}. R = {(a₁, a₂), (a₁, a₃), ...}. V(p) = {a₁, a₂...}, V(q) = {a₂, a₃...}. 67 68 Valuation can also be written as V(a₁) = {p}, etc. 69 70 ### 1b 71 #### 1b i 72 M, a₁ ⊨ □ □ (p ∨ q) 73 - R[a₁] = {a₂, a₃, a₄} (the successors of a₁). 74 - Holds by looking at the picture. 75 76 #### 1b ii 77 M, a₂ ⊨ ◇ q → ◇ ◇ q 78 - R[a₂] = {a₅}. 79 - Since a₅ ⊭ q, then a₂ ⊭ ◇ q. 80 - So formula holds because ◇ q doesn't hold. 81 82 ### 1d 83 Change V by making p true in all states. 84 85 ## 3 86 ### 3a 87 ⊨ □ (p → q) → (◇ p → ◇ q) 88 - Take an arbitrary pointed model (W,R),V,x. 89 - Assume x ⊨ □ (p → q), aim to show x ⊨ ◇ p → ◇ q. 90 - Assume x ⊨ ◇ p, aim to show x ⊨ ◇ q. 91 - x ⊨ ◇ p so x has a successor: there is y ∈ W such that y ⊨ p and Rxy. 92 - Because Rxy, we have x ⊨ ◇ q. 93 - So x ⊨ ◇ p → ◇ q. 94 - So x ⊨ □ (p → q) → (◇ p → ◇ q). 95 - Because x is arbitrary, the formula is universally valid. 96 97 Remember: □ φ is true if no successor, ◇ φ is false if no successor. 98 99 ### 3b 100 ⊨ □ (p ∧ q) → (◇ p ∧ ◇ q) 101 - Not valid with a singleton state and no relations. Premise is true, but not the right-hand side. 102 103 ### 3c 104 □ (□ p → p) → □ p 105 106 No. 107 Counterexample: 108 109  110 111 <details> 112 <summary>Dot code</summary> 113 114 ```dot 115 digraph g { 116 rankdir="LR" 117 1 -> 2 118 2 -> 3 119 3 -> 4 120 } 121 ``` 122 123 </details> 124 125 ## 4 126 First, draw a picture: 127 128  129 130 <details> 131 <summary>Dot code</summary> 132 133 ```dot 134 digraph g { 135 1 [label="1", xlabel="p"] 136 2 [label="2", xlabel="p"] 137 1 -> 3 138 1 -> 4 139 2 -> 1 140 3 -> 2 141 3 -> 3 142 4 -> 3 143 } 144 ``` 145 146 </details> 147 148 Then, create a tree: 149 150  151 152 <details> 153 <summary>Dot code</summary> 154 155 ```dot 156 digraph g { 157 root [label="M, 1 ⊨ ◇ □ ◇ p", xlabel="Turn: V"] 158 l11 [label="M, 4 ⊨ □ ◇ p", xlabel="Turn: F"]; root -> l11 159 r11 [label="M, 3 ⊨ □ ◇ p", xlabel="Turn: F"]; root -> r11 160 161 // right branch 162 r21 [label="M, 3 ⊨ ◇ p", xlabel="Turn: V"]; r11 -> r21 163 r31 [label="M, 2 ⊨ p."]; r21 -> r31; r31 -> r41; r41 [label="Verifier wins."] 164 r32 [label="M, 3 ⊨ p."]; r21 -> r32; r32 -> r42; r42 [label="Falsifier wins."] 165 166 r22 [label="M, 2 ⊨ ◇ p", xlabel="Turn: V"]; r11 -> r22 167 r33 [label="M, 1 ⊨ p."]; r22 -> r33; r33 -> r43; r43 [label="Verifier wins."] 168 169 // left branch 170 l11 -> r21 171 } 172 ``` 173 174 </details> 175 176 We cannot influence falsifier here since we play as verifier (trying to show that it holds). 177 But no matter what falsifier does, verifier has a winning strategy. 178