正规模态逻辑

正规系统把“必然”当成一种尊重有效推理的运算。若 $A\to B$ 在每个相关情形都成立，而且 $A$ 在每个相关情形都成立，那么 $B$ 也在每个相关情形成立，这就是 K 公理。若 $A$ 根本是不依赖任何假设的逻辑定理，那么在每个世界重申它仍然成立，这就是必然化。

这两个原则没有声称当前世界属于自己的可达范围，也没有声称可达关系能继续传递。因而“所有正规逻辑都认可”与“关于知识或时间听起来合理”是两种判断。后者必须用附加公理及其框架条件精确表达。

正规规则可以推出 $\square$ 保持定理等价。若 ${⊢}_{L}A\leftrightarrow B$，分别对 $A\to B$ 与 $B\to A$ 必然化，再各用一次 K 与 modus ponens，得到

同理可导出

正向使用命题定理 $A\to (B\to A\wedge B)$ 的必然化与两次 K，反向则必然化两个投影定理。这个推导展示分配能力来自 K 与规则，而不是把 $\square$ 当作普通字符串前缀。

错误的必然化可从一个开放假设看出。由假设 $p$ 当然能推出 $p$；若据此推出 $\square p$，就会把“当前世界偶然满足 $p$”升级成“所有可达世界都满足 $p$”。在有边 $wRv$、$p$ 仅在 $w$ 为真的模型中，前者真而后者假。因此局部假设不能无条件送入方框。

正规逻辑也不自动接受 $\square A\to A$。在没有自环的世界，所有后继满足 $A$ 与当前世界满足 $A$ 没有必然联系。类似地，$\square A\to ◻◻A$ 需要传递性，$\square A\to \diamond A$ 需要串行性；把这些额外公式写进“正规”的定义会抹去不同模态系统的结构差异。

模态逻辑 K公理库K 模态逻辑Modal logic K · System K由全部命题重言式、K 公理、modus ponens、代入与必然化生成的最小正规模态逻辑。是所有正规模态逻辑的交，也是只用上述公理与规则生成的最小系统。更强的正规逻辑可按包含关系组织成格；添加公理会缩小相应反模型类，却可能改变有限模型性质、复杂度和典范性。

Kripke 语义中，K 公理在每个框架上有效，必然化也保持框架有效性，因此正规系统天然适配关系语义。反向并非每个正规逻辑都由某个初等可定义的框架类完整刻画；Kripke 完备性、有限框架完备性和一阶可定义性是彼此不同的性质。

Gödel 翻译公理库Gödel 翻译Gödel translation · Gödel–McKinsey–Tarski translation给原子与蕴涵加上必然算子，把直觉主义命题逻辑忠实嵌入模态逻辑 S4。的目标 S4 是一个正规模态逻辑：它在 K 上加入 T 与 4。翻译正确性依赖这两条附加原则，不能只因 K 已经正规就把目标降为任意正规系统。