模态逻辑 我们先从最基础的概念开始。模态逻辑是对经典逻辑的扩展，它引入了“模态”运算符，用以表达“可能性”、“必然性”、“时间性”、“信念”等超出简单真假的范畴。最核心的模态逻辑是 命题模态逻辑 。 基本语法 命题模态逻辑的语言是在经典命题逻辑的基础上，增加了两个一元模态运算符： □ （通常表示“必然”） ◊ （通常表示“可能”） 其形成规则是：如果 φ 是一个合式公式，那么 □φ 和 ◊φ 也是合式公式。通常，我们将 ◊φ 定义为 ¬□¬φ ，意思是“可能φ”等价于“并非必然非φ”。 可能世界语义 为模态逻辑提供模型的是索尔·克里普克提出的 可能世界语义学 ，也称为 关系语义 或 克里普克语义 。一个克里普克模型 M 是一个三元组 〈W, R, V〉 ： W 是一个非空集合，其中的元素称为 可能世界 。你可以将每个世界 w ∈ W 想象成事物可能存在的一种状态或方式。 R 是 W 上的一个二元关系，称为 可及关系 。 w R u 表示世界 u 从世界 w 是“可想象的”或“可及的”。 V 是一个 赋值函数 ，它为每个命题变元 p 指定在哪些世界中为真。即， V(p) ⊆ W 。 真值定义 在模型 M 中，公式 φ 在世界 w 上为真（记作 M, w ⊨ φ ）的定义是递归的： M, w ⊨ p 当且仅当 w ∈ V(p) （对于命题变元）。 对于经典逻辑连接词（如 ¬ , ∧ ）的定义与命题逻辑相同，但所有真值都是相对于一个世界 w 而言的。 关键定义 ： M, w ⊨ □φ 当且仅当对于每一个满足 w R u 的世界 u ∈ W ，都有 M, u ⊨ φ 。 通俗地说：在世界 w 上，“必然φ”为真，当且仅当在所有 w 所能“看到”的世界 u 中， φ 都为真。 根据定义， M, w ⊨ ◊φ 当且仅当存在某个满足 w R u 的世界 u ∈ W ，使得 M, u ⊨ φ 。 通俗地说：在世界 w 上，“可能φ”为真，当且仅当存在至少一个 w 所能“看到”的世界 u ，其中 φ 为真。 模态逻辑系统与对应理论 不同的模态逻辑系统通过对可及关系 R 施加不同的性质来定义。这些性质对应着一些重要的公理模式： 系统 K ：最基本的系统，只要求 R 是任意关系。其核心公理是 K公理 ： □(p → q) → (□p → □q) 。 系统 T ：在 K 的基础上增加 T公理 ： □p → p 。这要求可及关系 R 是 自反的 （即对每个世界 w ，都有 w R w ）。因为如果 □p 在 w 上为真，根据自反性， w 自身是可及的世界，所以 p 在 w 上必须为真。 系统 S4 ：在 T 的基础上增加 4公理 ： □p → □□p 。这要求可及关系 R 是 自反且传递的 。传递性保证了“必然性”的必然性。 系统 S5 ：在 S4 的基础上增加 B公理 ： p → □◊p （或等价公理 ◊p → □◊p ）。这要求可及关系 R 是 自反、对称且传递的 ，即一个等价关系。在这种系统中，可及关系将所有世界划分为互通的“集群”，模态的视野变得全局化。 模态逻辑的应用 模态逻辑的框架非常通用，通过重新解释 □ 和 R 的含义，它可以应用于众多领域： 认知逻辑 ：将 □φ 解释为“智能体 A 知道 φ ”，可及关系 w R u 解释为“在世界 w 上，智能体 A 认为世界 u 是可能的”。 道义逻辑 ：将 □φ 解释为“ φ 是应当的/义务的”。 时态逻辑 ：将 W 解释为时间点的集合， R 解释为时间上的先后关系。 □φ 可解释为“将来总是 φ ”， ◊φ 解释为“在将来的某个时刻 φ ”。 动态逻辑 ：将 □ 替换为 [α] ，其中 α 是一个程序/动作。 [α]φ 表示“在执行动作 α 之后， φ 必然成立”。可及关系 w R_α u 表示“通过执行动作 α 可以从状态 w 转移到状态 u ”。