计算机科学家逻辑/模态逻辑/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$ 成立。