Kripke 模型过滤法 | Codeboy's Blog

形式陈述

设 $\mathcal M=(W,R,V)$ 是Kripke 模型， $Σ$ 是有限且对子公式封闭的模态公式集。在 $W$ 上定义

x\equiv_\Sigma y \iff \forall A\in\Sigma\; (\mathcal M,x\Vdash A\iff\mathcal M,y\Vdash A),

其中 $⊩$ 是模态满足关系。过滤后的世界集为商集 $W_\Sigma=W/{\equiv_\Sigma}$ ，世界 $x$ 的等价类记为 $[x]$ 。因为每个类由 $Σ$ 中公式的真值向量决定，

|W_\Sigma|\le 2^{|\Sigma|}.

对 $p\in\Sigma$ 定义 $V_\Sigma(p)=\{[x]:\mathcal M,x\Vdash p\}$ ；其他原子的赋值可以任取，因为过滤引理只承诺保持 $Σ$ 中公式。商关系常夹在两条边界关系之间：

[x]R_{\min}[y] \iff \exists x'\in[x]\;\exists y'\in[y]\;(x'Ry'),

\begin{aligned} [x]R_{\max}[y]\iff{}& \bigl[\forall\square B\in\Sigma\; (\mathcal M,x\Vdash\square B\Rightarrow\mathcal M,y\Vdash B)\bigr]\\ &\land \bigl[\forall\diamond B\in\Sigma\; (\mathcal M,y\Vdash B\Rightarrow\mathcal M,x\Vdash\diamond B)\bigr]. \end{aligned}

本页允许 $\square$ 与 $\diamond$ 都直接出现在公式中，因此两条限制都要检查。若事先把 $\diamond B$ 展开为 $\neg\square\neg B$ ，并对展开后的语法取子公式闭包，才可只写方框条件。子公式封闭保证 $R_{\max}$ 的两条限制都不依赖代表元。原边的代表满足这两条语义条件，所以 $R_{\min}\subseteq R_{\max}$ 。任取满足

R_{\min}\subseteq R_\Sigma\subseteq R_{\max}

的关系，得到过滤模型 $\mathcal M_\Sigma=(W_\Sigma,R_\Sigma,V_\Sigma)$ 。过滤引理断言：对每个 $A\in\Sigma$ ，

\mathcal M,x\Vdash A \iff \mathcal M_\Sigma,[x]\Vdash A.

证明对公式结构归纳。原子与布尔联结词直接由等价类和归纳假设处理。原来为真的 $\square B$ 对每条商边仍成立，因为 $R_\Sigma\subseteq R_{\max}$ 的方框条款保证目标满足 $B$ ；原来为假的 $\square B$ 有一个原边反例， $R_{\min}\subseteq R_\Sigma$ 保留它。原来为真的 $\diamond B$ 同样沿原边保留见证；若商模型新出现一个满足 $B$ 的后继， $R_{\max}$ 的菱形条款又迫使原世界已经满足 $\diamond B$ ，所以不会凭空造出新的菱形真值。

直觉

过滤法只保留目标公式真正能够提出的问题。若两个世界对 $Σ$ 中每个公式都给出相同答案，模态语言在这次任务里就无法区分它们，可以合并成一个状态。世界可能无限多，有限公式的真假档案却最多只有 $2^{|\Sigma|}$ 种。

关系不能直接任意投影。 $R_{\min}$ 保证原模型中真实存在的边不会丢失见证， $R_{\max}$ 保证新添的商边不会违反已经为真的方框义务。把商关系夹在两者之间，正好同时支持菱形的见证方向与方框的全称方向。

例子与边界

取无限模型 $W=\mathbb N$ ，只有边 $nR(n+1)$ ，并令 $p$ 恰在偶数世界为真。选

\Sigma=\{p,\square p\}.

偶数 $2k$ 满足 $p$ 、不满足 $□p$ ；奇数 $2k+1$ 不满足 $p$ 、满足 $□p$ 。因此所有世界只分成偶类 $E$ 与奇类 $O$ 。最小商关系有 $E R_{\min}O$ 与 $O R_{\min}E$ ，过滤后的两世界环准确保留 $Σ$ 中两条公式在每类的真值。无限链的具体位置消失了，奇偶交替这一层可观察行为仍在。

若 $Σ$ 含 $□p$ 却不含其子公式 $p$ ，两个对 $□p$ 看法相同、对 $p$ 看法不同的世界可能被错误合并；随后商模型无法稳定定义后继对 $p$ 的义务。对子公式封闭不是排版习惯，而是结构归纳能够落到下一层公式的必要条件。

菱形条款不能无条件省略。取两个没有任何边的世界 $u,v$ ，只让 $v$ 满足 $p$ ，并取 $\Sigma=\{p,\diamond p\}$ 。两个世界原来都不满足 $\diamond p$ 。若只检查方框条件，因 $\Sigma$ 没有方框公式，所谓最大关系会允许全部商边；新边 $[u]R_\Sigma[v]$ 就把 $\diamond p$ 错误变成真。上面的第二条限制正好禁止这条边。

过滤也不自动保留所有框架性质。 $R_{\min}$ 可能破坏传递性， $R_{\max}$ 又可能加入过多边而破坏其他条件。证明 S4、S5 或某个公理化框架类具有有限模型性质时，必须选择并验证适合该类的过滤关系；K 的无约束框架不面临这项额外责任。

推论与应用

若公式 $A$ 在某模型世界为真，取 $\Sigma=\operatorname{Sub}(A)$ ，过滤引理给出至多 $2^{|\Sigma|}$ 个世界的有限模型仍使 $A$ 为真。对反模型同理，这直接证明 K 的有限模型性质。

有限上界还给出朴素判定过程：枚举不超过该界的有点模型并检查 $A$ 或 $¬A$ 。这个过程远非最优，但把“存在有限见证”提升为可终止搜索需要一个可计算的界；只有抽象的有限模型性质而没有有效信息时，不能直接宣称得到算法。

过滤等价按一组公式的真值定义，模态互模拟则用原子、forth、back 的局部条件定义。二者都保留模态公式，却服务于不同任务：过滤主动压缩一个模型，互模拟比较两个模型的行为；过滤商映射也不必天然就是互模拟。

参考资料

Richard Zach, Boxes and Diamonds: An Open Introduction to Modal Logic，§§5.3–5.4, Definitions 5.4、5.9 与 Theorem 5.5：同时处理方框与菱形的过滤条件及真值保持。
Patrick Blackburn, Maarten de Rijke, and Yde Venema, Modal Logic, Cambridge University Press, 2001, Chapter 2, “Model Constructions,” filtration section。
Alexander Chagrov and Michael Zakharyaschev, Modal Logic, Oxford University Press, 1997, Chapter 5, canonical models and filtration。
Brian F. Chellas, Modal Logic: An Introduction, Cambridge University Press, 1980, §3.6, filtration。

形式陈述 ​

反向链接

形式陈述