K 模态逻辑

K 只保留方框作为全称后继量词必然满足的规律。它允许死端、自环缺失、不可逆边和任意长的非传递链，因此可以作为其他正规系统的共同底座。研究附加公理时，从 K 开始能准确看出结论究竟用了哪一项关系假设。

把方框看成后继集上的全称量词，还能解释 K 为何恰好停在这里。全称量词会保持定理和有限合取，也会把逐点成立的蕴涵传递给结论；这些都是 K 已经证明的规律。可是一次量化并不告诉我们当前点是否也在后继集中，更不保证后继的后继仍是当前点的后继。于是，$◻A$ 与 $◻◻A$ 分别检查一步与两步后继；在传递框架上，两步后继包含在一步后继中，才保证 $◻A\to ◻◻A$。

反模型可以显示一个附加公理需要什么关系性质。例如，要由“所有后继满足 $A$”推出“当前世界满足 $A$”，自反边就能把当前世界纳入检查；这正是 T 公理对应自反性的原因。

K 可推出正规单调性规则：若 ${⊢}_{\mathbf{K}}A\to B$，先必然化得到 $⊢◻(A\to B)$，再与 K 公理作 modus ponens，便有

取 $A=p\wedge q$、$B=p$，得到 $\square (p\wedge q)\to ◻p$。该推导只使用命题定理和正规规则，所以在任意关系图上成立。

三个小反模型划清 K 的边界。第一，单世界 $w$ 无自环，令 $p$ 在 $w$ 假；因后继为空，$\square p$ 真而 $p$ 假，所以 T 公理 $\square p\to p$ 不是 K 定理。第二，取三个世界 $w,v,u$，只有边 $wRv,vRu$，令 $p$ 在 $v$ 真、在 $u$ 假；于是 $w⊩◻p$ 但 $w⊮◻◻p$，所以 4 不是 K 定理。第三，死端世界使 $\square p$ 真、$◇p$ 假，所以 D 也不可导。

K 中 $◇A$ 定义为 $\mathrm{\neg }◻\mathrm{\neg }A$：经典否定把“并非所有后继都不满足 $A$”转成“存在满足 $A$ 的后继”。它与 $\square A$ 对后继提出不同要求；上面的死端例子就使 $\square A$ 成立而 $◇A$ 失败。

典范模态模型理路模态逻辑的典范模型Canonical modal model · Canonical model for K以最大一致公式集为世界、由方框义务定义可达边的句法生成 Kripke 模型。以最大 K-一致集为世界，并把方框公式决定的义务变成可达关系。典范模型定理理路模态逻辑典范模型定理Canonical model theorem for modal logic · Truth lemma for modal KK 的典范模型中公式在世界为真，当且仅当公式属于对应的最大一致集。由此证明 K 的强完备性和紧致性。

Kripke 模型过滤法理路Kripke 模型过滤法Kripke model filtration · Filtration method in modal logic按有限公式集的真值类型合并世界，并在商模型中保持这些公式满足性的有限化方法。把 K 的任意反模型压缩到只区分有限子公式的模型。对单个公式 $A$，世界数可控制在 $2^{|\mathrm{Sub}(A)|}$ 以内，因此 K 具有有限模型性质理路有限模型性质Finite model property · FMP每个不可导公式都已有有限反模型、等价地逻辑由其有限语义结构决定的性质。并可判定。这个上界来自子公式真值类型的数量，具体反模型还可以更小。

K 也是框架对应理论的基线。加入 T 得到自反框架逻辑，加入 4 得到传递框架逻辑，同时加入 T、4 得到 S4；加入 5 时涉及 Euclidean 条件。各扩展的可靠性、完备性与有限模型构造依赖相应的框架条件。