模态逻辑典范模型定理

典范模型把句法集合当世界，真值引理证明这种命名没有造假：集合里写着的公式恰好就是语义上成立的公式。布尔联结词靠最大一致性保持，模态算子靠关系与存在引理保持。于是“没有证明 $A$”可以转化成“某个世界使 $A$ 为假”，句法失败获得了可检查的语义见证。

这条对应是完备性证明的闭环。构造世界时只使用一致性，构造边时只使用方框义务；真值引理最终证明这两种局部设计共同实现了整套模态语言，而不是只实现原子和一层方框。

K 不证明 T 公理 $\square p\to p$。可先用一个无后继、且 $p$ 为假的单点模型验证公式集 $\{◻p,\mathrm{\neg }p\}$ 与 K 相容，再把它扩张为最大一致集 $\Gamma$。真值引理立即给出

所以典范模型内部已经含有 T 的反例。这里的单点模型只用于借 K 的可靠性确认一致性；最终反例由典范构造统一提供。

由 $\mathrm{\Gamma }{⊬}_{\mathbf{K}}A$ 得到反模型时，真正一致的是 $\mathrm{\Gamma }\cup \{\mathrm{\neg }A\}$ 的每个有限相关部分；扩张为最大一致集后，真值引理让全部 $\Gamma$ 为真而 $A$ 为假。这给出强完备性。若只从“$A$ 不是定理”开始，则取 $\Gamma =\varnothing$，得到普通完备性。

边界在于证明系统。把 K 换成扩展 $L$ 后，仍可建立 $L$-最大一致集和真值引理，但若要相对于某个受限框架类完备，还需证明 $L$ 的典范框架属于该类。某些正常逻辑不是典范逻辑；真值引理本身成立，不代表目标关系性质会在典范框架中出现。

强完备性给出

因为形式证明只使用有限多个前提，强完备性还导出语义紧致性：若 $\Gamma$ 的每个有限子集都有 Kripke 模型，则 $\Gamma$ 整体有模型。这个结论不提供有限模型，典范世界集通常仍然无限。

要从完备性走向可判定性，还需过滤法公理库Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。或其他有限模型构造。典范模型保证反模型存在，过滤法只保留目标公式的有限观察类型；有限模型性质公理库有限模型性质Finite model property · FMP每个不可导公式都已有有限反模型、等价地逻辑由其有限语义结构决定的性质。由后一步而非真值引理单独推出。

典范法还提供一致性集实现、框架对应和插值等研究的起点。不过每项后继结论都有额外条件：例如插值需要更细的句法分离，复杂度上界需要有效搜索，不能把“有典范反模型”直接改写成“能高效找到反模型”。