認識論理の導入

(数式を中央にもっていくとか定理環境などレイアウトがうまくいってません. わかり次第更新したいです. )

認識論理は様相論理の一分野です.

具体的には, 様相オペレーターとして $K_i$ を導入し, $K_i\phi$ を「agent $i$ は $\phi$ を知っている」と解釈します.
また, 関係記号として $\mathcal{K}_i$ を導入し, $(s,t)\in\mathcal{K}_i$ を「agent $i$ が世界 $s$ の情報が与えられたときに $t$ が可能であると考えている」と解釈します.

認識論理において有用な概念としてcommon knowledgeとdistributed knowlwdgeというものがあり, まず具体例を用いてこれらのイメージを紹介します.
たとえば, AさんとBさんが映画Cを見た後, AさんがBさんに「この映画どうだった？」と聞いたとします.
このとき, Bさんが適切に答えるために, まずAさんとBさんは「この映画は映画Cを指す」ことを知っている必要があります.
この「この映画は映画Cを指す」ことを $p$ で表すとすると, さらにAさんはBさんが $p$ を知っていることを知っている必要があります.
さらに, BさんはAさんがBさんが $p$ を知っていることを知っていることを知っている必要があり, これがずっと繰り返されます.
このようにずっと繰り返されたものがなりたつとき, $p$ をcommon knowledgeといいます.

また, ある事実 $\phi$ がグループのdistributed knowledgeであるというのは, グループ内のagentの知識を集めたとき $\phi$ を推論できる, ということです.

例えば, Dさんは「FさんはGさんまたはHさんが好き」という知識を, Eさんは「FさんはHさんを好きでない」という知識を持っているとします.
このときDさんとEさんというグループは「FさんはGさんが好き」というdistributed knowledgeをもっていることになります.

このようなイメージのもとに, 定義を与えていきます.

認識論理における論理式 $\phi$ は以下のように定義されます.

$\phi::=p~|~\lnot\phi~|~\phi\lor\psi~|~K_i\phi$

ただし, $\Phi$ を命題記号全体の集合として $p\in\Phi$ です.

この各 $i$ をagentといいます.

また, 通常の様相論理と同じようにしてKripke structureを構成します.

組 $M=(S,\mathcal{K}_1,\dots,\mathcal{K}_n,V)$ が以下をみたすとき, $M$ を Kripke structureといいます.

$S$ は集合.
各 $\mathcal{K}_i$ は $S$ 上の2項関係.
$V:\Phi\to\mathcal{P}(S)$ .

充足関係は, 論理式の一番外側の記号が様相オペレーターのときだけを見ればよいでしょう.

$M=(S,\mathcal{K}_1,\dots,\mathcal{K}_n,V)$ をstructure, $s\in S$ , $G\subseteq \{1,\dots,n\}$ (この $G$ をgroupという)としたとき, 以下が定義です.

$(M,s)\vDash K_i\psi\iff(s,t)\in \mathcal{K}_i$ をみたす任意の $t$ に対して $(M,t)\vDash\psi$
$(M,s)\vDash E_G\phi\iff$ 任意の $i\in G$ に対して $(M,s)\vDash K_i\phi$ .
$(M,s)\vDash C_G\phi\iff k=1,2,\dots$ に対して $(M,s)\vDash E_G^k\phi$
$(M,s)\vDash D_G\phi\iff(s,t)\in\bigcap_{i\in G}\mathcal{K}_i$ をみたす任意の $t$ に対して $(M,t)\vDash\phi$

ただし, $E_G^1=E_G$ , $E_G^{k+1}=E_G^k$ とし, また, $G$ が明らかなときは省略することもあります.

各解釈として, $E_G\phi$ は「 $G$ の全ての人が $\phi$ を知っている. 」, $C_G\phi$ は「 $\phi$ は $G$ のagentのcommon knowledgeである. 」, $D_G\phi$ は「 $\phi$ は $G$ のagentのdistriguted knowledgeである. 」と定めます.

これらの定義が一番最初に説明した解釈と一致していることがわかるかと思います.