Kripke 模型过滤法

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

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

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

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

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

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

若公式 $A$ 在某模型世界为真，取 $\mathrm{\Sigma }=\mathrm{Sub}(A)$，过滤引理给出至多 $2^{|\mathrm{\Sigma }|}$ 个世界的有限模型仍使 $A$ 为真。对反模型同理，这直接证明 K 的有限模型性质公理库有限模型性质Finite model property · FMP每个不可导公式都已有有限反模型、等价地逻辑由其有限语义结构决定的性质。。

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

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