模态逻辑典范模型定理

典范模型把最大一致的公式集当作世界，真值引理把“公式属于集合”与“公式在这个世界为真”联系起来。最大一致性保证布尔联结词的行为，典范关系和存在引理保证模态算子的行为；结构归纳把这条对应推广到任意复杂的公式。

于是，要为一个不可证公式 $A$ 找反例，可以先构造含 $\mathrm{\neg }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\}$ 一致：否则一个只用有限多个前提的矛盾证明会给出 $\mathrm{\Gamma }{⊢}_{\mathbf{K}}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每个不可导公式都已有有限反模型、等价地逻辑由其有限语义结构决定的性质。由后一步而非真值引理单独推出。

典范法也为插值与复杂度研究提供起点：插值证明进一步分析前提与结论如何共享语言，复杂度分析则需要能有效构造和搜索反模型的方法。