lectures.alex.balgavy.eu

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

modal-logic.html (4110B)

      1 <html>
      2 <head>
      3     <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script>
      4     <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
      5     <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css">
      6     <link rel="Stylesheet" type="text/css" href="style.css" />
      7     <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
      8     <script>
      9       document.addEventListener('DOMContentLoaded', function() {
     10         document.querySelectorAll('pre.code').forEach(function(item) {
     11           hljs.highlightBlock(item)
     12         })
     13       });
     14     </script>
     15     <title>modal-logic</title>
     16 </head>
     17 <body>
     18 <style type="text/css">
     19 nav a {
     20     text-align: left;
     21 }
     22 nav #name {
     23     text-align: right;
     24     float: right;
     25     font-style: italic;
     26 }
     27 </style>
     28     <nav>
     29     <a href="index.html">Index</a>
     30     <span id="name">Alex Balgavy</span>
     31     </nav>
     32     <hr>
     33     <div class="content">
     34     
     35 <div id="Modal logic"><h2 id="Modal logic" class="header"><a href="#Modal logic">Modal logic</a></h2></div>
     36 <p>
     37 modal logic allows reasoning about dynamics -- futures, knowledge, beliefs, etc.
     38 </p>
     39 
     40 <p>
     41 modalities (unary connectives):
     42 </p>
     43 <ul>
     44 <li>
     45 □ (box): sure, always, has to be, knows, guaranteed (kinda like ∀)
     46 
     47 <li>
     48 ◇ (diamond): possibly, sometimes, maybe, believes is possible, possible result (kinda like ∃)
     49 
     50 </ul>
     51 
     52 <p>
     53 Kripke model <code>M = (W, R, L)</code> consists of:
     54 </p>
     55 <ul>
     56 <li>
     57 W worlds
     58 
     59 <li>
     60 R accessibility relation
     61 
     62 <li>
     63 L labeling function: which propositional letters are true in which world (<code>w ⊩ p ↔ p ∈ L(w)</code>)
     64 
     65 </ul>
     66 
     67 <p>
     68 Kripke models define truth <em>per world</em>.
     69 </p>
     70 
     71 <p>
     72 <img src="img/kripke-model-and-graph.png" alt="Kripke model and graph" />
     73 </p>
     74 
     75 <div id="Modal logic-Truth in worlds"><h3 id="Truth in worlds" class="header"><a href="#Modal logic-Truth in worlds">Truth in worlds</a></h3></div>
     76 <p>
     77 <code>M, w ⊩ Φ</code> means formula Φ is true in world w of Kripke model M.
     78 </p>
     79 
     80 <p>
     81 ◇ Φ is true in world w if there exists a world w' such that R(w, w') and Φ is true in w'.
     82 </p>
     83 
     84 <p>
     85 □ Φ is true in world w if Φ is true in all worlds w' with R(w, w'). special case when world has no outgoing edge, ◇ Φ never holds and □ Φ always holds.
     86 </p>
     87 
     88 <div id="Modal logic-Truth in Kripke models"><h3 id="Truth in Kripke models" class="header"><a href="#Modal logic-Truth in Kripke models">Truth in Kripke models</a></h3></div>
     89 <p>
     90 Φ is true in Kripke model <code>M = (W, R, L)</code> (i.e. M ⊨ Φ), iff x ⊩ Φ for every world x ∈ W.
     91 </p>
     92 
     93 <p>
     94 all propositional tautologies also hold in modal logic.
     95 </p>
     96 
     97 <div id="Modal logic-Semantic implication/entailment"><h3 id="Semantic implication/entailment" class="header"><a href="#Modal logic-Semantic implication/entailment">Semantic implication/entailment</a></h3></div>
     98 <p>
     99 M,w ⊨ ψ in every world w in every Kripke model where M,w ⊨ Φ₁, ..., M,w ⊨ Φn.
    100 </p>
    101 
    102 <p>
    103 modal validity: ⊨ ψ if in every world w in ever Kripke model M holds M,w ⊨ ψ.
    104 </p>
    105 
    106 <p>
    107 modal logical equivalence: <code>Φ ≡ ψ</code> if <code>M,w ⊨ Φ ↔ M,w ⊨ ψ</code>. in other words, Φ ≡ ψ ↔ Φ ⊨ ψ and ψ ⊨ Φ.
    108 </p>
    109 
    110 <div id="Modal logic-Frames"><h3 id="Frames" class="header"><a href="#Modal logic-Frames">Frames</a></h3></div>
    111 <p>
    112 frame: Kripke model without labeling. <code>F = (W,R)</code>, W worlds, R accessibility relation
    113 </p>
    114 
    115 <p>
    116 Φ is valid in frame F (i.e. F ⊨ Φ) if for <em>every</em> labeling L, Kripke model M = (W,R,L) makes Φ true.
    117 </p>
    118 
    119 <p>
    120 Correspondence of formulas and frame properties
    121 </p>
    122 <ul>
    123 <li>
    124 reflexive:
    125 
    126 <ul>
    127 <li>
    128 F ⊨ □ p → p
    129 
    130 <li>
    131 F ⊨ p → ◇ p
    132 
    133 </ul>
    134 <li>
    135 symmetric:
    136 
    137 <ul>
    138 <li>
    139 F ⊨ q → □ ◇ q
    140 
    141 <li>
    142 F ⊨ ◇ □ p → p
    143 
    144 </ul>
    145 <li>
    146 transitive:
    147 
    148 <ul>
    149 <li>
    150 F ⊨ □ p → □ □ p
    151 
    152 <li>
    153 F ⊨ ◇ ◇ p → ◇ p
    154 
    155 </ul>
    156 <li>
    157 serial:
    158 
    159 <ul>
    160 <li>
    161 F ⊨ ◇ T
    162 
    163 <li>
    164 F ⊨ □ p → ◇ p
    165 
    166 </ul>
    167 <li>
    168 functional: □ p ↔ ◇ p
    169 
    170 </ul>
    171 
    172     </div>
    173 </body>
    174 </html>