index.md (1548B)
1 +++ 2 title = 'Exercise 4' 3 +++ 4 # Exercise 4 5 "show that x not derivable": use soundness and completeness. 6 show that there is frame in the right class. 7 8 ¬ □ ¬ □ p → p not derivable in S4 (I think reflexive + transitive) 9 10  11 12 <details> 13 <summary>Graphviz code</summary> 14 15 <!-- :Tangle(dot) diagram.dot --> 16 ```dot 17 digraph g { 18 rankdir=LR 19 1 -> 1 20 2 -> 2 21 2 -> 1 22 2 [xlabel="(¬ p)"] 23 } 24 ``` 25 26 </details> 27 28 Derivation of ¬ □ ¬ □ p → p in S5: 29 1. S5 has as axiom ¬ □ p → □ ¬ □ p 30 2. ¬ □ ¬ □ p → □ p. prop contrapositive 1 31 3. □ p → p. axiom A1. 32 4. ¬ □ ¬ □ p → p. prop 2, 3. 33 34 ## Exercise sheet 5 35 ### 1a 36 N = (ℕ, <). ◇ □ p → □ ◇ p? 37 1. take arbitrary valuation for N, M=(N,V). 38 2. Take M ∈ N. 39 3. Assume n ⊨ ◇ □ p. Goal to show n ⊨ □ ◇ p. 40 4. Take x arbitrary successor of n. Goal x ⊨ ◇ p. 41 5. x + n > x and x + n ⊨ p. 42 6. So x ⊨ ◇ p...and so the formula valid. 43 44 ### 4b 45 Until is not modally definable in BML. 46 * Until defined with M,t ⊨ φ U ψ ↔ ∃ v, t < v, v ⊨ ψ, ∀x t < x < v and x ⊨ φ. 47 * temporal frame, so irreflexive and transitive 48 49 Proof: 50 - create two models M where a ⊨ p U q, M' where a' ⊭ p U q. 51 - claim bisimilar by giving bisimulation, states a and a'. 52 - because a and a' bisimilar, are modally equivalent. 53 - suppose that until is definable in BML by a formula ζ(x, y) 54 - then we have a ⊨ p U q, so a ⊨ ζ(p, q). Opposite for a'. 55 - contradiction, a and a' modally equivalent but satisfy different formulas (i.e. a ⊨ ζ but a' ⊭ ζ).