Kripke 框架

框架像一座尚未填入内容的舞台：世界是位置，可达边规定每个位置能看见哪些位置。换一组命题赋值只是重新布置灯光与道具；若一个公式无论怎样布置都成立，才说明它捕捉了舞台结构本身。

这也解释了为什么关系公理能对应模态公理。要检测自反性，赋值可以故意让 $p$ 在某个非自反世界为假、却在它看见的所有世界为真；$\square p\to p$ 随即失败。公式不是直接读取“自反”这个标签，而是利用任意赋值探测缺少的边。

取线性框架

且没有其他边。它既不自反也不传递，因为 $w_0$ 没有直接到 $w_2$ 的边。加上三个自环只得到自反闭包，仍不自动包含 $w_{0}R{w}_2$；再加入这条边才同时满足当前有限图上的传递要求。

在单点框架 $W=\{w\}$ 上有两种不同关系。若 $R=\varnothing$，则每个 $\square \phi$ 都在 $w$ 真，因为没有后继可作反例，而每个 $◇\phi$ 都假。若 $R=\{(w,w)\}$，则 $\square \phi$ 与 $\phi$ 在 $w$ 同真同假。世界数相同并不能决定模态行为，边才决定量化范围。

本库约定 $W$ 非空。若允许空框架，则每个公式都会因“对所有世界”没有反例而框架有效，许多完备性和反模型陈述需要额外排除这个退化对象。另一个边界是：框架同构保留全部模态有效式，但非同构框架也可能拥有同一套有效式，所以有效式集合通常不能恢复原图。

给框架加入赋值便得到Kripke 模型公理库Kripke 模型Kripke model · Relational modal model在 Kripke 框架上为命题变量逐世界赋值而得到的模态语义模型。；模态满足关系公理库模态满足关系Modal satisfaction relation · Kripke semantics for modal logic递归规定模态公式在 Kripke 模型某一世界何时为真的关系。随后区分点满足、模型全局满足与框架有效。三层量词不可交换：某个点满足、某个固定赋值下所有点满足、所有赋值下所有点满足分别是逐步增强的断言。

模态逻辑 K公理库K 模态逻辑Modal logic K · System K由全部命题重言式、K 公理、modus ponens、代入与必然化生成的最小正规模态逻辑。由所有 Kripke 框架刻画。限制到自反、传递或等价关系框架会得到更强逻辑，因为允许的反模型减少。反过来，并非任意模态公理都有一个简单的一阶关系条件与之对应；“看起来像关系性质”不足以代替对应性证明。

在有限模型方法中，过滤法公理库Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。会从模型构造有限商框架。若目标逻辑要求传递或 Euclidean 等性质，还必须选择能保持该框架类的过滤关系；仅仅把世界按公式真值合并，并不自动保留所有关系条件。