index.md (5399B)
1 +++ 2 title = 'Exercise class 3' 3 +++ 4 5 # Exercise class 3 6 ## Exercise 1 7 The two models: 8 9 <table> 10 <tr> 11 <th>M</th> 12 <th>K</th> 13 </tr> 14 <tr> 15 <td> 16 <img src="1-model-m.dot.svg" alt="Model M"> 17 18 <details> 19 <summary>Graphviz code</summary> 20 21 <!-- :Tangle(dot) 1-model-m.dot --> 22 ```dot 23 digraph g { 24 a -> b 25 a -> c 26 c -> a 27 c -> d 28 } 29 ``` 30 31 </details> 32 33 </td> 34 <td><img src="1-model-k.dot.svg" alt="Model K"> 35 36 <details> 37 <summary>Graphviz code</summary> 38 39 <!-- :Tangle(dot) 1-model-k.dot --> 40 ```dot 41 digraph g { 42 1 -> 2 43 2 -> 3 44 3 -> 1 45 1 -> 4 46 } 47 ``` 48 49 </details> 50 </td> 51 </tr> 52 </table> 53 54 ### a) 55 56 | Round | S | D | link | local harmony | 57 |-------|--------|--------------|-------|---------------| 58 | 0 | | | a ~ 1 | ok | 59 | 1 | a -> c | (1/2) 1 -> 2 | c ~ 2 | ok | 60 | 2 | c -> d | 2 -> 3 | d ~ 3 | ok | 61 | 3 | 3 -> 1 | stuck. | | | 62 | ... | ... | ... | ... | ... | 63 | 1 | a -> c | (2/2) 1 -> 4 | c ~ 4 | ok | 64 | 2 | c -> a | stuck. | | | 65 66 So even in an optimal game, D gets stuck. 67 Therefore, M,a and K,1 are not bisimilar. 68 69 Once we find a winning strategy for S no matter what D does, we can stop. 70 71 ### b) 72 A formula distinguishing M,a and K,1 is: ◇ ◇ □ ⊥ 73 74 In two steps, we reach a blind state. 75 76 ## Sequents and tableaux (exercise 5) 77 ### □ p → ◇ p 78 Show validity of: □ p → ◇ p 79 80 Pre-processing: 81 82 ``` 83 □ p → ◇ p ≡ ¬ □ p ∨ ◇ p 84 ≡ ◇ ¬ p ∨ ◇ p 85 ``` 86 87 <table> 88 <tr><th>Sequent</th><th>Tableau</th></tr> 89 <tr> 90 <td> 91 92 ``` 93 ⇒ ◇ ¬ p ∨ ◇ p 94 ⇒ ◇ ¬ p, ◇ p 95 ``` 96 97 Stuck. No diamond on left, so cannot take a step. 98 99 ◇ ¬ p ∨ ◇ p not valid, so □ p → ◇ p not valid. 100 </td> 101 <td> 102 <img src="5-1-tableau.dot.svg" alt="Tableau" /> 103 104 Zero non-solid successors. Stuck, does not close, so non-validity. 105 106 Counter-model F = ({1}, ∅), V(p) = ∅. 107 108 <details> 109 <summary>Graphviz code</summary> 110 111 <!-- :Tangle(dot) 5-1-tableau.dot --> 112 ```dot 113 graph g { 114 a [label="* ◇ ¬ p ∨ ◇ p", xlabel="1"] 115 a -- b 116 b [label="* ◇ ¬ p, ◇ p", xlabel="1"] 117 } 118 ``` 119 120 </details> 121 122 </td> 123 </tr> 124 </table> 125 126 ### □ (p → q) → (□ p → □ q) 127 Show validity of: □ (p → q) → (□ p → □ q) 128 129 Pre-processing: 130 131 ``` 132 □ (p → q) → (□ p → □ q) ≡ ¬ ◇ ¬ (¬ p ∨ q) → (¬ ◇ ¬ p → ¬ ◇ ¬ q) 133 ≡ ◇ ¬ (¬ p ∨ q) ∨ (◇ ¬ p ∨ ¬ ◇ ¬ q) 134 ≡ ◇ (p ∧ ¬ q) ∨ ◇ ¬ p ∨ ¬ ◇ ¬ q 135 ``` 136 137 <table> 138 <tr> <th>Sequent</th> <th>Tableau</th> </tr> 139 <tr> 140 <td> 141 142 ``` 143 ⇒ ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q 144 ◇ ¬ q ⇒ ◇ (p ∧ ¬ q), ◇ ¬ p 145 146 One case: 147 ¬ q ⇒ p ∧ ¬ q, ¬ p 148 p, ¬ q ⇒ p ∧ ¬ q 149 p ⇒ p ∧ ¬ q, q 150 151 Two goals, both must be valid: 152 A) p ⇒ p, q 153 Valid. 154 B) p ⇒ ¬ q, q 155 p, q ⇒ q 156 Valid. 157 158 Sequent is valid, so initial formula is valid. 159 ``` 160 161 </td> 162 <td> 163 <img src="5-2-tableau.dot.svg" alt="Tableau" /> 164 165 Closes, so initial formula is valid. 166 167 <details> 168 <summary>Graphviz code</summary> 169 170 <!-- :Tangle(dot) 5-2-tableau.dot --> 171 ```dot 172 graph g { 173 a [label="* ◇ (p ∧ ¬ q), ◇ ¬ p, ¬ ◇ ¬ q", xlabel="1"] 174 b [label="◇ ¬ q * ◇ (p ∧ ¬ q), ◇ ¬ p", xlabel="1"]; a -- b 175 c [label="¬ q * p ∧ ¬ q, ¬ p", xlabel="2"]; b -- c [style="dashed"] 176 d [label="p * p ∧ ¬ q, q", xlabel="2"]; c -- d 177 178 el [shape="record", label="{ p * p, q | closes. }", xlabel="2"]; d -- el 179 180 er [label="p * ¬ q, q", xlabel="2"]; d -- er 181 f [shape="record", label="{ p, q * q | closes. }", xlabel="2"]; er -- f 182 } 183 ``` 184 185 </details> 186 187 </td> 188 </tr> 189 </table> 190 191 ### (□ p → □ q) → □ (p → q) 192 Show validity of: (□ p → □ q) → □ (p → q) 193 194 Pre-processing: 195 196 ``` 197 (□ p → □ q) → □ (p → q) ≡ (¬ ◇ ¬ p → ¬ ◇ ¬ q) → ¬ ◇ ¬ (¬ p ∨ q) 198 ≡ ¬ (◇ ¬ p ∨ ¬ ◇ ¬ q) ∨ ¬ ◇ (p ∧ ¬ q) 199 ≡ (¬ ◇ ¬ p ∧ ◇ ¬ q) ∨ ¬ ◇ (p ∧ ¬ q) 200 ``` 201 202 Tableau: 203 204  205 206 <details> 207 <summary>Graphviz code</summary> 208 209 <!-- :Tangle(dot) 5-3-tableau.dot --> 210 ```dot 211 graph g { 212 a [label="* (¬ ◇ ¬ p ∧ ◇ ¬ q), ¬ ◇ (p ∧ ¬ q)", xlabel="1"] 213 b [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p ∧ ◇ ¬ q", xlabel="1"]; a -- b 214 215 la [label="◇ (p ∧ ¬ q) * ¬ ◇ ¬ p", xlabel="1"]; a -- la 216 lb [label="◇ (p ∧ ¬ q), ◇ ¬ p *", xlabel="1"]; la -- lb 217 218 lla [label="p ∧ ¬ q *", xlabel="2"]; lb -- lla [style="dashed"] 219 llb [label="p, ¬ q *", xlabel="2"]; lla -- llb 220 llc [label="{p * q | does not close}", xlabel="2", shape="record"]; llb -- llc 221 222 lra [label="{¬ p * | does not close}", xlabel="3", shape="record"]; lb -- lra [style="dashed"] 223 224 ra [label="◇ (p ∧ ¬ q) * ◇ ¬ q", xlabel="1"]; b -- ra 225 rb [label="p ∧ ¬ q * ¬ q", xlabel="4"]; ra -- rb [style="dashed"] 226 rc [label="p ∧ ¬ q, q *", xlabel="4"]; rb -- rc 227 rd [label="p, ¬ q, q *", xlabel="4"]; rc -- rd 228 re [label="{p, q * q | closes}", xlabel="4", shape="record"]; rd -- re 229 } 230 ``` 231 232 </details> 233 234 This yields a counter-model: 235 236  237 238 <details> 239 <summary>Graphviz code</summary> 240 241 <!-- :Tangle(dot) 5-3-counter-model.dot --> 242 ```dot 243 digraph g { 244 rankdir=LR 245 1 -> 2; 2 [shape="Mrecord", label="{2 | p}"] 246 1 -> 3 247 } 248 ``` 249 250 </details> 251 252 1 ⊭ □ (p → q) because 2 ⊭ p → q. 253 But 1 ⊨ (□ p → □ q) because 1 ⊭ □ p.