Kripke 模型 | Codeboy's Blog

形式陈述

固定命题变量集 $\mathsf{Prop}$ 。Kripke 模型是三元组

\mathcal M=(W,R,V),

其中 $(W,R)$ 是Kripke 框架，而赋值

V:\mathsf{Prop}\longrightarrow\mathcal P(W)

把每个命题变量 $p$ 映到使它为真的世界集合。等价地，可把 $V$ 写成 $W\times\mathsf{Prop}\to\{0,1\}$ 。这层赋值扩展了命题逻辑的单一真值赋值：同一个原子 $p$ 可以在不同世界取不同真值，模态算子再沿 $R$ 比较这些世界。

带指定世界的二元组 $(\mathcal M,w)$ 称为有点模型。模态公式的真假通常在有点模型上判断；模型本身满足 $φ$ 则约定为每个 $w\in W$ 都满足。若非空子集 $X\subseteq W$ 对后继封闭，即 $x\in X$ 且 $xRy$ 时必有 $y\in X$ ，那么把 $R,V$ 限制到 $X$ 得到生成子模型。它保留 $X$ 中各点可见的全部后继，因此保留这些点的所有基本模态公式真值。

模型同构是保持可达边和原子赋值的世界双射；同构有点模型满足完全相同的模态公式。反向一般不成立：模态语言只能观察沿边展开的行为，未必识别图的全部组合结构。

直觉

框架回答“从这里需要考虑哪些情形”，赋值回答“每个基本事实在哪些情形成立”。两部分缺一不可。只有赋值而没有边， $□$ 和 $◇$ 没有量化范围；只有边而没有赋值，关系结构存在，却无法开始递归判断任何含原子的公式。

有点模型把观察位置也纳入对象。同一张世界图在 $w_0$ 与 $w_1$ 处可能给出不同答案，不是因为模型改变，而是观察者拥有不同的后继集合。模态逻辑研究的正是这种“位置相关但按统一规则计算”的真值。

例子与边界

令 $W=\{s,t,u\}$ ，关系为 $sRt,sRu,tRu$ ，赋值取

V(p)=\{t,u\},\qquad V(q)=\{u\}.

在 $s$ 看来，两个直接后继都满足 $p$ ，但只有 $u$ 满足 $q$ ；在 $t$ 看来，唯一后继 $u$ 同时满足 $p,q$ 。这个模型足以区分“所有下一种情形满足 $p$ ”与“至少一种下一情形满足 $q$ ”，其中 $sRt$ 与 $tRu$ 确实组成从 $s$ 经 $t$ 到 $u$ 的两步路径，但这条路径本身不推出直接边 $sRu$ ；本例的原关系另外明确包含了这条直接边。

若把 $V(q)$ 改为 $\{t,u\}$ ，框架完全不变，但关于 $q$ 的公式真值会改变。反过来，保持赋值不动而删除 $sRu$ ，所有原子在各世界的真假都不变。在 $s$ 处，唯一剩下的直接后继 $t$ 仍满足 $p$ ，所以 $□p$ 仍为真；但 $t$ 不满足 $q$ ，所以 $◇q$ 从真变为假。模型的两个组成部分承担不同信息，不能用“世界状态”一个模糊词同时代替。

普通模态 Kripke 模型不要求赋值沿 $R$ 单调。即使 $wRv$ 且 $p$ 在 $w$ 真， $p$ 也可以在 $v$ 假。持久性是直觉主义 Kripke 语义额外加入的条件；把它无声放进一般模态模型会错误排除合法反模型。

推论与应用

模态满足关系把 $V$ 的原子情况递归扩张到布尔联结词和模态算子。一个公式在模型中全局为真，仍不等于它在底层框架上有效：框架有效还要对所有可能赋值重新检查。

典范模态模型把最大一致公式集当作世界，是从句法自动制造 Kripke 模型的特殊构造。过滤法则从已有模型出发，把对有限公式集无法区分的世界合并。一个展开句法，一个压缩语义，但二者都必须明确给出 $W,R,V$ ，并证明新模型的满足关系具有所需性质。

模态互模拟比较两个模型的原子赋值和逐步分支。互模拟不要求世界集合等大，也不要求存在全局双射；它只维护模态语言实际能追踪的局部行为，因此比模型同构弱得多。

参考资料

Patrick Blackburn, Maarten de Rijke, and Yde Venema, Modal Logic, Cambridge University Press, 2001, Chapter 2, models, generated submodels, and truth。
Alexander Chagrov and Michael Zakharyaschev, Modal Logic, Oxford University Press, 1997, Chapter 8, relational semantics。
Brian F. Chellas, Modal Logic: An Introduction, Cambridge University Press, 1980, Chapter 3, relational models。

形式陈述 ​

反向链接

形式陈述