index.md (1237B)
1 +++ 2 title = 'Multi-modal logic' 3 +++ 4 # Multi-modal logic 5 Assume set of labels I (which in a diagram are on the arrows). 6 For every label i there is modality 〈i〉 so the formulas of multi-modal logic are, given I, defined for i in ∈ I. 7 8 I-frame is pair (W, {Rᵢ | i ∈ I}). 9 Rᵢ ⊆ W × W for every i ⊆ I. 10 11 I-model is triple (W, {Rᵢ | i ⊆ I}, V). 12 13 ## Truth and validity 14 For M an I-model, M,w ⊨ φ is defined by induction on the definition of formulas. 15 16 Clauses: 17 - M,w ⊨ 〈a〉φ iff M,v ⊨ φ for some v with Rₐwv 18 - M,w ⊨ [a]φ iff M,v ⊨ φ for all v with Rₐwv 19 20 ## Example 21 Use index set I = {a, b, c}. 22 Give model with a world where the formula 〈a〉(〈b〉[a] p ∧ [c] ¬ 〈a〉p) is true. 23 24  25 26 <details> 27 <summary>Graphviz code</summary> 28 29 <!-- :Tangle(dot) example-multimodal-logic-formula.dot --> 30 ```dot 31 digraph g { 32 rankdir=LR 33 1 -> 2 [label="a"] 34 2 -> 3 [label="b"] 35 } 36 ``` 37 38 </details> 39 40 41 For a bisimulation, when you do a step between states, they have to be with the same label (so the mimic step must have the same label). 42 43 ## Geach axiom 44 ◇ □ p → □ ◇ p. 45 46 Valid in frame iff for every r ← s → u there is r → v ← u.