計算機科學家邏輯/模態邏輯/Kripke 語義

定義 1

Kripke 框架是一個對 $\langle W,R\rangle$，其中 $W$ 是一個非空集（可能的世界的集合），而 $R$ 是一個在 $W$ 上的二元關係。我們寫 $wRw'$ 當且僅當 $(w,w')\in R$，我們說世界 $w'$ 可以從世界 $w$ 訪問，或者說 $w'$ 可以從 $w$ 訪問，或者說 $w'$ 是 $w$ 的後繼。

Kripke 模型是一個三元組 $\langle W,R,V\rangle$，其中 $W$ 和 $R$ 如上所述，而 $V$ 是一個對映 ${\mathcal {P}}\mapsto 2^{W}$，其中 ${\mathcal {P}}$ 是命題變數的集合。 $V(p)$ 旨在表示在估值 $V$ 下命題 $p$ 為真的所有世界。

給定一個模型 $\langle W,R,V\rangle$ 和一個世界 $w\in W$，我們定義滿足關係 $\models$ 如下:

${\begin{matrix}w\models p&{\mbox{iff }}&w\in V(p)\\w\models \lnot A&{\mbox{iff }}&w\not \models A\\w\models A\land B&{\mbox{iff }}&w\models A{\mbox{ and }}w\models B\\w\models A\lor B&{\mbox{iff }}&w\models A{\mbox{ or }}w\models B\\w\models A\to B&{\mbox{iff }}&w\not \models A{\mbox{ or }}w\models B\\w\models \Box A&{\mbox{iff }}&{\mbox{for all }}v\in W,(w,v)\not \in R{\mbox{ or }}v\models A\\w\models \diamond A&{\mbox{iff }}&{\mbox{there exists some }}v\in W,{\mbox{ with }}(w,v)\in R{\mbox{ and }}v\models A\\\end{matrix}}$

我們說 $w$ 滿足 $A$ 當且僅當 $w\models A$（不提及估值 $V$）。公式 $A$ 稱為在模型 $\langle W,R,V\rangle$ 中可滿足，當且僅當存在某些 $w\in W$，使得 $w\models A$。公式 $A$ 稱為在框架 $\langle W,R\rangle$ 中可滿足，當且僅當存在某些估值 $V$ 和某些世界 $w\in W$，使得 $w\models A$。公式 $A$ 稱為在模型 $\langle W,R,V\rangle$ 中有效，寫成 $\langle W,R,V\rangle \models A$ 當且僅當它在 $W$ 中的每個世界都為真。公式 $A$ 稱為在框架 $\langle W,R\rangle$ 中有效，寫成 $\langle W,R\rangle \models A$ 當且僅當它在所有模型 $\langle W,R,V\rangle$ 中有效。

引理 1

運算子 $\diamond$ 和 $\square$ 是對偶的，即對於所有公式 $A$ 和所有框架 $\langle W,R\rangle$，等價關係 $\diamond A\leftrightarrow \lnot \square \lnot A$ 成立。