Modální logika

Toto cvičení je spíše povídáním o modální logice. Modální logiky lze použít pro reprezentaci znalostí v multi-agentních systémech.

Modální logika je rozšířením klasické výrokové nebo predikátové logiky. V modální logice nemáme jen jediný svět, ale máme množinu tzv. „možných světů“ $W$. Dále máme binární relaci dostupnosti $R \subseteq W \times W$ na množině možných světů, kde $R(w, u)$ vyjadřuje, že svět $u$ je dostupný ze světa $w$. Obvykle je tato relace zapsána v infixovém zápisu jako $wRu$. Navíc máme funkci $v$, která pro každý možný svět dává model tohoto specifického světa (přiřazení pravdy ve výrokové logice nebo struktura v predikátové logice). Soubor možných světů a relace dostupnosti mezi nimi společně tvoří rámec $\langle W, R \rangle$.

Sémantika pro spojky a kvantifikátory je stejná jako v logice výrokové / predikátové a je dána ohodnocovací funkcí $v$ (ta se může lišit v každém možném světě). V modální logice však navíc definujeme nové modality $\square$ a $\diamond$, které lze použít jako unární logické spojky. Formule $\square P$ platí ve světě $w$, pokud platí v každém světě $u$ takovém, že $wRu$. Formule $\diamond P$ je pravdivá ve světě $w$, pokud je pravdivá v některém $u$ takovém, že $wRu$.

Jaký je význam nových modalit? To ve skutečnosti závisí na konkrétním případu použití modální logiky. Běžný význam je ten, že $\square P$ říká, že $P$ je nutně pravda (tj. pravda ve všech dostupných možných světech), zatímco $\diamond P$ říká, že $P$ je možná pravda (tj. pravda v některých dostupných možných světech).

V klasické modální logice jsou tyto dvě modality komplementární podobně jako $\forall$ a $\exists$ jsou v predikátové logice. To znamená, že $\square P \equiv \neg \diamond \neg P$ a $\diamond P \equiv \neg \square \neg P$. První z nich se čte v přirozeném jazyce jako „$P$ je nutné, pokud $\neg P$ není možné“, a druhý se čte jako „$P$ je možné, pokud jeho negace není nutná“.

Kripkeho sémantika

Definujme nyní sémantiku modální logiky formálněji. Jde o tzv. Kripkeho sémantiku možných světů. Mějme rámec $\langle W, R \rangle$ a ohodnocení $v$, pak řekneme, že nějaká atomická formule $P$ platí ve světě $w$ ($w \vDash P$), pokud $v (w , P)$ (ohodnocení se chová jako relace, která platí pro dvojice svět, atomická formule pokud je atomická formule pravdivá v daném světě), dále

Formule $P$ platí v modelu $\langle W, R, v \rangle$, pokud $w \vDash P$ pro každý svět $w \in W$, a platí v rámci $\langle W, R \rangle$, pokud platí v $\langle W, R, v \rangle$ pro všechna možná ohodnocení $v$.

Obecně definovaná modální logika výše je poměrně slabá, hlavně proto, že nemáme žádné předpoklady o relaci dostupnosti. V praktických aplikacích často přidáváme další podmínky, abychom získali užitečnější systémy (viz níže).

Systémy modální logiky

Kromě výše uvedené sémantické definice můžeme modální logiku definovat také syntakticky rozšířením výrokové nebo predikátové logiky o další axiomy a pravidla. To, jaké axiomy a pravidla přidáváme, závisí na zamýšlené aplikaci konkrétního systému modální logiky.

Určitě musíme přidat symboly pro obě modality a definovat je jako komplementární, jak jsme to udělali výše. Většina systémů modální logiky (tzv. normální modální logiky) také obsahují následující pravidlo $\bf{N}$ a axiom $\bf{K}$

Přidání pouze těchto dvou axiomů nám dává tzv. $K$ systém (pojmenovaný po Saulovi Kripke, autorovi sémantiky možných světů). Tento systém je stále velmi slabý a nedokazuje ani to, že je-li něco nutné, je to také pravdivé. To však lze přidat jako axiom $\bf{T}$

Existují také jiné běžné axiomy, které můžeme najít v mnoha systémech modální logiky

Přidáním některých z těchto axiomů pak vzniknou různé systémy modální logiky (které mohou mít různé aplikace), například výše uvedený systém $K$ používá pouze axiomy $\bf{N}$ a $\bf{K}$. Pokud přidáme také $\bf{T}$, dostaneme systém, který se běžně nazývá $T$. Systémy s názvem $S4$ a $S5$ získáme přidáním $\bf{4}$ respektive $\bf{5}$ do $T$. Nakonec systém $D$ se získá přidáním axiomu $\bf{D}$ do systému $K$.

Existuje ekvivalence mezi axiomy a různými podmínkami na relaci dostupnosti. Například systém $K$ odpovídá obecné modální logice bez jakýchkoli předpokladů ohledně relace dostupnosti. Axiom $T$ zajišťuje, že relace dostupnosti je reflexivní. Axiom $\bf{4}$ zaručuje, že je tranzitivní a axiom $\bf{5}$ zajišťuje, že relace je Euclidovská (pro každé $u$, $t$, $w$, pokud $wRu$ a $wRt$ pak $uRt$). Euklidovská vlastnost spolu s reflexivitou také implikuje symetrii a tranzitivitu.

Výše uvedená diskuse o vztazích mezi axiomy a předpoklady o relaci dostupnosti vede k pozorování, že v modelech systému $T$ je relace dostupnosti reflexivní, v modelech $S4$ je reflexivní a tranzitivní a v modelech $S5$ je to ekvivalence.

Multimodální logika

Někdy je užitečné mít více než jeden pár modalit (viz epistemická logika níže). Pokud máme sadu $n$ modalit ${\square_1, \dots, \square_n}$, nazýváme výslednou logiku $n$-modální. Komplementární modality $\diamond_1, \dots, \diamond_n$ jsou v tomto případě obvykle definovány jako $\diamond_i P \equiv \neg \square_i \neg P$. Sémantika multimodální logiky je přirozeným rozšířením sémantiky výše popsané modální logiky, nicméně nyní máme $n$ relací dostupnosti $R_1, \dots, R_n$. Modalita $\square_i$ je pak vyhodnocena vzhledem k relaci dostupnosti $R_i$.

Epistemic modal logic

Epistemická modální logika je jedním z typů modální logiky, které jsou zvláště důležité pro multiagentní systémy. Tento typ logiky nám umožňuje uvažovat o tom, co agenti vědí. Je to multimodální logika s modalitami $K_i$ vyjadřující, že agent $i$ něco ví. Je také zcela běžné přidávat další modality $E_G$ vyjadřující, že každý agent ve skupině $G$ něco ví (pro konečné skupiny agentů ji lze definovat jako $E_G P \equiv \bigwedge K_i P$). V epistemické logice obvykle předpokládáme, že relace dostupnosti je ekvivalence a dostupné možné světy jsou někdy nazývány nerozlišitelnými světy. Toto jsou světy, v nichž se může agent nacházet na základě svých znalostí. Pokud například nevím, zda venku prší, mohu být ve dvou možných světech - v jednom, kde venku prší, a v jiném, kde neprší.

Další užitečnou modalitou je $C_G$ vyjadřující, že něco je ve skupině $G$ obecně známo (common knowledge). Obecná znalost je zajímavý pojem. Znamená nejen to, že každý agent něco ví, ale navíc to znamená, že každý agent ví, že každý agent tu věc ví, a každý agent ví, že každý agent ví, že každý agent tu věc ví a tak dále až do nekonečna. Obecné znalosti mohou mít silné důsledky, jak obvykle ukazuje řada logických indukčních hádanek. Nejznámější z nich je Muddy Children Puzzle.

Dalším zajímavým konceptem jsou distribuované znalosti vyjádřené pomocí modality $D_G$. Je to kombinovaná znalost skupiny agentů. Představte si, že máme dva lidi, ani jeden z nich neví, jestli venku prší, nicméně jeden z nich ví, že jejich kamarádka nosí červený kabát, jen když prší, a druhý právě viděl tuto kamarádku v červeném kabátě. Kombinací těchto dvou informací mohou odvodit, že venku prší, proto je tato skutečnost jejich distribuovanou znalostí.

V epistemické logice se používá většina výše uvedených axiomů, ale některé z nich mají nové názvy.

Je snadné zkontrolovat, že tyto axiomy přímo odpovídají obecným axiomům definovaným výše (konkrétně tvoří systém $S5$), to také ukazuje, že modální logika může být užitečná pro reprezentaci znalostí. Chceme-li místo toho reprezentovat beliefs (typicky označené jako $B_i$ vyjádřující, že agent $i$ něčemu věří), budeme muset odstranit axiom pravdy, protože někdy agenti mohou věřit něčemu, co není pravda. Obvykle tento axiom nahrazujeme axiomem

Doxastická logika

Doxastická logika je logika o beliefs. Používá modální operátor $B$, který vyjadřuje, že agent věří, že něco je pravdivé. Agentům v doxastické logice se říká dokazovače a je jich celá řada typů s rostoucí mírou racionality.

Například dokazovač prvního typu má plnou znalost výrokové logiky a nakonec uvěří všem tautologiím. Jeho beliefs jsou uzavřeny na pravidlo modus ponens (pokud věří $p$ a $p \to q$, bude časem věřit i $q$). Tyto podmínky lze zapsat jako

Typ 1* je dokazovač, který si je o něco více vědom sám sebe, protože má navíc podmínku, která označuje, že nejenže dle modus ponens bude věřit $q$, ale že dokonce i věří tomu, že $q$ bude věřit

Dokazovač typu 2 se navíc věří, že jeho beliefs jsou uzavřeny pod modus ponens

Dokazovač typu 3 je normální dokazovač typu 2, tj.

Dokazovač typu 4 je dokazovač typu 3, který navíc věří, že je normální, tj.

Temporální logika

Temporální logika je dalším typem multimodální logiky. Tento typ umožňuje agentům uvažovat o čase. Existuje řada různých typů temporální logiky v závislosti na tom, co předpokládají o čase. Například v lineární temporální logice (LTL) je čas lineární tj. relace dostupnosti (která v tomto případě říká, jaké světy jsou možné v dalším časovém kroku) je lineární uspořádání, ve výpočetní stromové logice (Computation Tree Logic - CTL) se čas může v budoucnosti větvit jako strom a předpokládá se, že jedna z větví v budoucnosti nastane. Logika CTL je užitečná pro popis chování počítačových programů a při formálním ověřování softwaru.

V LTL máme dvě modality - $X$ a $U$. Modalita $X$ vyjadřuje, že v dalším kroku bude něco pravda. Modalita $U$ je binární a $A U B$ znamená, že $A$ platí alespoň do té doby, než $B$ bude platit, což musí nastat teď nebo v někdy v budoucnu. Existují i další modality definované pomocí těchto základních

CTL má možnost větvení času v budoucnosti a používá řadu časových modalit a operátorů

Odkazy a další čtení

Pokud se chcete dozvědět více o modální logice, doporučuji si přečíst následující zdroje (většinou stránky z Wikipedie) - ty byly použity k napsání většiny textu zde.

  1. Modal Logic @ Wikipedia
  2. Kripke semantics @ Wikipedia
  3. Doxastic Logic @ Wikipedia
  4. Temporal Logic @ Wikipedia
  5. Linear Temporal Logic @ Wikipedia
  6. Computation Tree Logic @ Wikipedia
  7. Epistemic Logic @ Wikipedia
  8. Epistemic Logic @ Stanford Encyclopedia of Philosophy
  9. Modal Logic (chapter 5) in Nerode, Anil, and Richard A. Shore. Logic for applications. Springer Science & Business Media, 2012.
Mgr. Martin Pilát, Ph.D.
Malostranské náměstí 25
118 00 Praha
Martin.Pilat@mff.cuni.cz