Modálne logiky

Základne pojmy

Modálne logiky sú rozsiahlou a vyvíjajúcou sa oblasťou logických systémov s aplikáciou v mnohých disciplínach, vrátane informatiky. Prvotná formulácia modálnej logiky z konca devätnásteho resp. začiatku dvadsiateho storočia pozostávala z rozšírenia jazyka výrokovej logiky o modalitu je nutné, že označovanú symbolov $\square$, kde význam formuly $$\square \varphi,$$ je možné vysloviť ako: "je nutné, že $\varphi$".

V súčasnosti existuje mnoho druhov modálnych logík, ktoré obsahujú viacero modalít (multimodálne logiky), ktoré dokážu modelovať rôzne vlastnosti reálneho sveta ako napr.:

• aletická logika nutnosti a možnosti,
• temporálna logika narábajúca s časom,
• deontická logika zaoberajúca sa príkazmi, zákazmi či povoleniami,
• epistemická logika ktorá popisuje objektívne poznanie a racionálne presvedčenie,
• BDI logika ako logika troch modalít: presvedčenia, prianí, a zámerov,
• a mnoho ďalších.

V rámci tohto cvičenia sa budeme venovať modálnym logikám ktoré narábajú s aletickými operátormi nutnosti a možnosti. Začneme základnou modálnou logikou $K$, pomenovanou po priekopníkovi v oblasti modálnych logík Saulovi Kripkemu, ktorý formuloval princípy sémantickej metódy nazvanej sémantika možných svetov, prostredníctvom ktorej, je možno formálne definovať sémantiku jednotlivých modálnych logík.

Jazyk modálnej logiky

Jazyk modálnej logiky je rozšírením jazyka klasickej výrokovej logiky o modality:

• je nutné, že $\square$,
• je možné, že $\diamondsuit$.

Podobne ako operátor negácie $\neg$ vo výrokovej, obe modality sú unárne logické spojky, ktoré majú najvyššiu prioritu.

Platia nasledujúce De Morganove ekvivalencie: $$ \begin{array}{rcl} \neg \square \neg \varphi & \equiv & \diamondsuit \varphi, \\ \neg \diamondsuit \neg \varphi & \equiv & \square \varphi. \end{array} $$

Syntax modálnej logiky

Syntax modálnej logiky je definovaná produkčným pravidlom v Backus-Naurovej forme, prostredníctvom ktorého je možné konštruovať všetky prípustné tvary formúl: $$ \varphi ::= p \mid \top ~\mid ~⊥~ \mid \neg\varphi \mid \varphi \land \psi \mid \varphi \lor \psi \mid \varphi \Rightarrow \psi \mid \square\varphi \mid \diamondsuit\varphi. $$ Množinu všetkých formúl ktorú opisuje uvedená gramatika označíme $Mprop$. Syntax modálnej logiky rozširuje syntax výrokovej logiky o aletické modálne operátory. Kde:

• $p$ je množina atomických formúl.
• $\top, \perp$ sú konštanty jazyka, nazývané verum, absurdum.
• $\neg\varphi$ negácia, číta sa neplatí že $\varphi$,
• $\varphi \land \psi$ konjunkcia, číta sa platí, že $\varphi$ a zároveň platí, že $\psi$,
• $\varphi \lor \psi$ disjunkcia, číta sa platí, že $\varphi$ a resp. alebo platí, že $\psi$,
• $\varphi \Rightarrow \psi$ implikácia, číta sa ak platí, že $\varphi$ potom platí, že $\psi$.
• $\square\varphi$ modálny operátor nutnosti, číta sa je nutné, že $\varphi$,
• $\diamondsuit\varphi$ modálny operátor možnosti, číta sa je možné, že $\varphi$.

Asociativita a priorita spojok ostáva rovnaká ako v prípade výrokovej logiky, avšak modálne operátory $\square, \diamondsuit$ majú spolu s negáciou najvyššiu prioritu.

Dedukčné kalkuly

Dedukčné kalkuly modálnej logiky rozširujú kalkul výrokovej logiky o ďalšie axiómy modálnej logiky. Na základe prijatých axióm sa modálne logiky sa rozdeľujú nasledovne:

Základná modálna logika K a jej kalkul K

Rozširuje kalkul výrokovej logiky o:

• distributívnu axiómu: $$\square (φ ⇒ ψ) ⇒ (\square φ ⇒ \square ψ) \quad (K),$$
• pravidlo nutnosti: $$φ \vdash \square φ \quad (nec).$$

Modálna logika T a jej kalkul T

Je niekedy nazývaná aj $M$. Rozširuje kalkul K o axiómu: $$\square φ ⇒ φ \quad (T).$$

Modálna logika S4 a jej kalkul S4

Rozširuje kalkul T o axiómu: $$\square φ ⇒ \square \square φ \quad (S4).$$

Modálna logika S5 a jej kalkul S5

Rozširuje kalkul T o axiómu: $$\diamondsuit φ ⇒ \square \diamondsuit φ \quad (S4).$$

Modálna logika B a jej kalkul B

Rozširuje kalkul T o axiómu: $$ φ ⇒ \square \diamondsuit φ \quad (B).$$

Sémantika modálnej logiky

Formálne možno definovať sémantiku modálnej logiky prostredníctvom sémantiky možných svetov. Táto metóda pozostáva s definície Kripkeho modelu.

Kripkeho model modálnej logiky je usporiadaná trojica: $$M=(W, ≤, ⊩),$$ kde:

• $W$ je neprázdna množina možných svetov v tvare $W = \{x_1, x_2,...\}$.
• $≤$ je relácia dosiahnuteľnosti na svetoch $≤ \subseteq W × W$.
• $⊩$ je relácia platnosti formuly vo svete $⊩ ⊆ W × Mprop$.

Zároveň:

• Jednotlivé svety je možné chápať ako stavy, prostredia, vrcholy a podobne.
• Zápis $x_1 ≤ x_2$ je možné prečítať ako "zo sveta $x_1$ je možné dosiahnuť svet $x_2$" alebo "svet $x_2$ je dosiahnuteľný zo sveta $x_1$".
• Zápis $x⊩p$ je možné prečítať ako "vo svete $x$ platí atomický výrok $p$".

Reláciu platnosti definujeme vzhľadom na syntax jazyka: $$ \begin{array}{lcl} x⊩p & \text{potom} & ∀x' \quad \text{ak}\quad x≤x' \quad\text{potom}\quad x'⊩p \\ x⊩φ ∧ ψ & \text{vtt.} & x⊩φ \quad \text{a} \quad x⊩ψ\\ x⊩φ ∨ ψ & \text{vtt.} & x⊩φ \quad \text{alebo} \quad x⊩ψ \\ x⊩φ ⇒ ψ & \text{vtt.} & (\text{ak} \quad x⊯φ \quad \text{alebo} \quad x⊩ψ) \\ x⊩ ¬φ & \text{vtt.} & (x ⊯ φ)\\ x⊩ \square φ & \text{vtt.} & ∀x', x≤x' (x' ⊩ φ)\\ x⊩ \square φ & \text{vtt.} & \cancel ∃ x', x≤x'\\ x⊩ \diamondsuit φ & \text{vtt.} & ∃x', x≤x' (x' ⊩ φ)\\ x⊯ \diamondsuit φ & \text{vtt.} & \cancel ∃ x', x≤x' \end{array} $$

Definícia relácia platnosti hovorí:

• Prvý riadok opisuje pravidlo perzistencie. To znamená ak atomický výrok $p$ platí v určitom svete $x$, potom platí v každom svete $x'$ z neho dosiahnuteľnom.
• Druhý riadok definuje konjunkciu a to tak, že formula $φ ∧ ψ$ platí vo svete $x$ ak $x⊩φ$ a zároveň $x⊩ψ$.
• Tretí riadok definuje disjunkcia tak, že formula $φ ∨ ψ$ platí vo svete $x$ ak platí $x⊩φ$ alebo $x⊩ψ$.
• Štvrtý riadok definuje implikáciu. Formula $φ ⇒ ψ$ platí vo svete $x$, ak formula $φ$ neplatí vo svete $x$ alebo formula $ψ$ platí vo svete $x$.
• Piaty riadok definuje negáciu. Formula $¬φ$ platí vo svete $x$ ak vo všetkých z neho dosiahnuteľných svetoch $x'$, formula neplatí $x' ⊯ φ$.
• Šiesty a siedmy riadok definuje modálny operátor nutnosti nasledovne:
  • Šiesty riadok hovorí, že formula $\square φ$ platí vo svete $x$ ak vo všetkých z neho dosiahnuteľných svetoch $x'$ platí formula $φ$.
  • Siedmy riadok hovorí, že ak zo sveta $x$ nie je dosiahnuteľný žiadny svet, potom platí formula $\square φ$.
• Ôsmy a deviaty riadok definuje modálny operátor možnosti nasledovne:
  • Ôsmy riadok hovorí, že formula $\diamondsuit φ$ platí vo svete $x$ ak existuje aspoň jeden z neho dosiahnuteľný svet $x'$, kde platí formula $φ$.
  • Deviaty riadok hovorí, že ak zo sveta $x$ nie je dosiahnuteľný žiadny svet, potom neplatí formula $\diamondsuit φ$.

Relácia dosiahnuteľnosti má v závislosti od jednotlivých logík rozdielne vlastnosti. Tieto vlastnosti sú zhrnuté v nasledujúcej tabuľke: