模态逻辑的典范模型

典范模型把“一个世界知道哪些公式”反过来当作世界本身。最大一致性使每个公式在世界里都有明确立场，又禁止同时接受矛盾。方框公式则像交给所有后继的合同：若 $\square A$ 属于 $\Gamma$，每个 $\Gamma$-后继都必须包含 $A$。

菱形公式提出存在性要求。$◇A$ 不只是“没有写下 $\square \mathrm{\neg }A$”，存在引理还要构造一个同时接受 $A$、又履行全部方框合同的相容后继。这个句法可实现性正是典范模型能把未证明公式变成语义反例的铰链。

设最大一致集 $\Gamma$ 包含

存在引理给出后继 $\Delta$，其中 $q\in \mathrm{\Delta }$；由可达关系定义，$q\to r$ 与 $r\to s$ 也都属于 $\Delta$。最大一致集对 modus ponens 封闭，所以 $r,s\in \mathrm{\Delta }$。这个例子展示后继并非随意拼凑：菱形提供见证目标，方框提供每个后继都必须承担的约束。

不能把世界换成任意一致集而保持同样简单的真值论证。若某个一致集既不含 $A$ 也不含 $\neg A$，公式成员关系就无法直接给出完整的经典真值；最大化正是为了让布尔归纳闭合。另一方面，最大一致不表示集合有限、可计算或由单个公式生成，典范模型通常非常大。

典范关系也不是原语义框架的“真实可达性”。它由证明系统设计，用于证明完备性。对 K，它无需满足额外关系性质；对加入公理的扩展，能否从公理推出典范关系具有所需性质，是典范性证明的实质，不能只沿用 K 的构造名称。

典范模型定理公理库模态逻辑典范模型定理Canonical model theorem for modal logic · Truth lemma for modal KK 的典范模型中公式在世界为真，当且仅当公式属于对应的最大一致集。证明

因此任何 K-一致公式集都在典范模型某个世界同时实现，任何 K 不可导公式都拥有 Kripke 反模型。存在引理负责模态归纳的反向，Lindenbaum 引理负责把局部一致信息补成世界。

典范模型也可用于分析附加公理。若能证明扩展逻辑的典范关系属于目标框架类，便得到相对于该类的强完备性；若公理在所有目标框架有效、典范框架却不保留相应条件，则简单典范法不够。这种失败说明证明技术需要加强，不等于逻辑本身必然不完备。

与过滤法公理库Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。相比，典范模型优先保证“所有一致句法类型都有世界”，过滤法优先只保留有限公式所能观察的差别。完备性通常先用前者得到反模型，有限模型性质再用后者把反模型压小。