模态逻辑与克里普克框架

父级：logic

在命题逻辑中加入算子 □（"必然 / 总是 / 可证"）和 ◇（"可能"）。它们的含义来自可能世界。

克里普克框架与语义

框架（frame）是一个二元组 (W, R)：一组世界 W，加一个可达关系 R ⊆ W×W。模型在此基础上为每个世界指派一份原子命题的赋值。那么在世界 w 处：

• □φ 成立，当且仅当 φ 在每一个满足 w R w' 的 w' 处成立；
• ◇φ 成立，当且仅当 φ 在某一个可达的 w' 处成立。

框架条件 ↔ 公理（对应理论）

R 的形状决定了哪些模态公理成立：

S4 = 自反 + 传递（可证性、拓扑、直觉主义逻辑）；S5 = 等价关系（知识、形而上学必然性）。

真正要紧的联系

• 直觉主义逻辑 = S4（哥德尔翻译）；而直觉主义逻辑本身也有自己的一套克里普克模型（世界 = 知识状态，且单调递增）——这正是通往 类型论 与 柯里–霍华德对应 的桥梁。
• 时序逻辑（LTL/CTL）= 关于时间的模态逻辑，而模型检验 = 无穷字上的自动机（Büchi）——这是一条深刻的逻辑 ↔ 自动机联系（Vardi–Wolper），回接到 自动机层级。
• 可证性逻辑（GL）： 把 □ 读作"在 PA 中可证"；勒布定理以模态的方式刻画了哥德尔不完备性（不完备性）。
• μ 演算： 模态逻辑 + 最小/最大不动点——涵盖了 LTL/CTL；其自然的不变量是互模拟（bisimulation）。

与主线的关联——这就是 harness 的骨架

递归 harness 的可能世界框架，字面意义上就是克里普克语义：

• 一次品味/调度选择 = 挑选一个世界 w；收敛是逐世界发生的；
• [[modal-status-labels|□ 确定 / ◇ 可能]]这套状态标签，就是这些模态算子；
• R（可达关系）= 一致性/依赖关系——"哪些延续路径与已作出的承诺保持一致"；收紧 = R 向单一被钉住的世界收缩；
• 漂移 = 在没有被 R 连接的世界之间游走。

克里普克的"世界"给了我们一套词汇，让我们能说："非确定性选择了一个世界；收敛与门控都是逐世界发生的。"