lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

index.md (3024B)

      1 +++
      2 title = 'Some midterm solutions'
      3 +++
      4 # Some midterm solutions
      5 ## Universal validity
      6 Is this formula universally valid: ◇ (p → q) → (◇ p → ◇ q)
      7 - Take arbitrary frame F = (W,R) and arbitrary valuation V for F.
      8 - Take arbitrary state x ∈ W
      9 - ? F,V,x ⊨ φ
     10 - Assume x ⊨ ◇ (p → q). That is: there is a state y ∈ W such that Rxy and y ⊨ p → q
     11 - Want to show x ⊨ ◇ p → ◇ q
     12 - Assume x ⊨ ◇ p. That is: there is a state z ∈ W such that Rxz and z ⊨ p.
     13 - Note: y and z are not necessarily the same! (but they might be)
     14 - Counter-model:
     15 
     16     ![Counter model diagram](counter-model.dot.svg)
     17 
     18     - 3 ⊨ p so 1 ⊨ ◇ p
     19     - 2 ⊨ ¬ p so 2 ⊨ p → q so 1 ⊨ ◇ (p → q)
     20     - 2 ⊭ q, 3 ⊭ q so 1 ⊭ ◇ q
     21 - By counter-model, the formula is not universally valid
     22 
     23 <details>
     24 <summary>Graphviz code</summary>
     25 
     26 <!-- :Tangle(dot) counter-model.dot -->
     27 ```dot
     28 digraph g {
     29 rankdir=LR
     30 1 -> 2
     31 1 -> 3
     32 3 [xlabel="p"]
     33 }
     34 ```
     35 
     36 </details>
     37 
     38 ## Formula for a statement
     39 "Has no blind successor": ¬ ◇ □ ⊥, □ ◇ T ("wherever I go, I can do a step"), □ ¬ □ ⊥
     40 
     41 "Has at least one non blind successor": ◇ ◇ T
     42 
     43 ## Bisimulation & contraction
     44 That question about two models, if asked say they are bisimilar, just give a bisimulation and say the pair consisting of the two states is in the bisimulation.
     45 
     46 The bisimulation contraction is then:
     47 
     48 ![Bisimulation contraction](bisimulation-contraction.dot.svg)
     49 
     50 <details>
     51 <summary>Graphviz code</summary>
     52 
     53 <!-- :Tangle(dot) bisimulation-contraction.dot -->
     54 ```dot
     55 digraph g {
     56 ac -> b
     57 b -> ac
     58 ac -> ac
     59 b [xlabel="[p]"]
     60 }
     61 ```
     62 
     63 </details>
     64 
     65 ## Global diamond
     66 Asked to see if global diamond is definable in basic modal logic (BML), as given by: M,x ⊨ E φ iff there is y ∈ W such that y ⊨ φ.
     67 (Side remark: if we can define it, the operator is like an abbreviation, it doesn't change the expressive power).
     68 
     69 Steps:
     70 - Suppose E is definable in BML by ζ.
     71 - Suppose Ep is definable in BML by ζ(p).
     72 - Consider the models:
     73 
     74     <table>
     75     <thead><th>M</th><th>N</th></thead>
     76     <tbody>
     77     <tr>
     78     <td>
     79 
     80     <img alt="Model M" src="model-m.dot.svg"/>
     81 
     82     <details>
     83     <summary>Graphviz code</summary>
     84 
     85     <!-- :Tangle(dot) model-m.dot -->
     86     ```dot
     87     digraph g {
     88     a
     89     b [label="b | [p]"]
     90     }
     91     ```
     92 
     93     </details>
     94     </td>
     95 
     96     <td>
     97 
     98     <img alt="Model N" src="model-n.dot.svg"/>
     99 
    100     <details>
    101     <summary>Graphviz code</summary>
    102 
    103     <!-- :Tangle(dot) model-n.dot -->
    104     ```dot
    105     digraph g {
    106     x
    107     }
    108     ```
    109 
    110     </details>
    111     </td>
    112     </tr>
    113     </tbody>
    114     </table>
    115 
    116 - We have M,a ⊨ Ep because M,b ⊨ p, so M,a ⊨ ζ(p).
    117 - N,x ⊭ Ep so N,x ⊭ ζ(p).
    118 - We have M,a bisimilar with N,x because Z = {(a,x)} is a bisimulation and (a,x) ∈ Z.
    119 - Because bisimilar states are modally equivalent, they must make true the same formulas in BML. So a ⊨ ζ(p) iff x ⊨ ζ(p).
    120 - Contradiction: N,x ⊭ ζ(p)
    121 - So, the assumption that E is definable in BML does not hold.
    122 - Therefore, E is not definable in BML.
    123 
    124