K 模态逻辑

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

“最弱”不等于没有内容。K 已经迫使方框尊重逻辑等价、合取和已证明的蕴涵；它拒绝的是关于当前世界与后继结构的额外承诺，而不是拒绝推理本身。

把方框看成后继集上的全称量词，还能解释 K 为何恰好停在这里。全称量词会保持定理和有限合取，也会把逐点成立的蕴涵传递给结论；这些都是 K 已经证明的规律。可是一次量化并不告诉我们当前点是否也在后继集中，更不保证后继的后继仍是当前点的后继。于是 $◻A$ 与 $◻◻A$ 在 K 中承担两层独立义务，不能像在传递框架上那样无条件合并。

这种克制使反模型诊断很清楚：公式失败时，先看它要求的是普通全称推理，还是偷偷假定了自反、传递、串行等图性质。前一种失败意味着推导本身有误；后一种失败则提示应当明确选择更强的模态系统，而不是把所需边性质藏进“必然”的自然语言读法。

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 定理。第二，取 $wRv,vRu$ 而没有 $wRu$，令 $p$ 在 $v$ 真、在 $u$ 假；可安排 $w⊩◻p$ 但 $w⊮◻◻p$，所以 4 不是 K 定理。第三，死端世界使 $\square p$ 真、$◇p$ 假，所以 D 也不可导。

K 中 $◇A$ 通常定义为 $\mathrm{\neg }◻\mathrm{\neg }A$。这个对偶使用经典否定；它不表示可达关系必须对称，也不把方框与菱形变成互逆运算。存在一个 $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 条件。名称相邻不意味着证明可以互换，每个扩展都要重新检查可靠性、完备性和有限模型构造是否保持其框架条件。