模态逻辑基础

模态逻辑（Modal Logic）是研究关于“必然性”和“可能性”的逻辑系统。它在传统命题逻辑的基础上，引入了模态算子来描述命题的模态属性。

核心算子

• 必然性算子 (Necessity Operator) □：表示命题在所有可达世界中均为真。
• 可能性算子 (Possibility Operator) ◊：表示命题在至少一个可达世界中为真。

算子关系

模态算子之间存在对偶关系：

• □P ≡ ¬◊¬P （必然 P 等价于 非可能非 P）
• ◊P ≡ ¬□¬P （可能 P 等价于 非必然非 P）

语义基础：克里普克语义 (Kripke Semantics)

模态逻辑通常通过“可能世界”模型来定义：

1. 可能世界集合 (W)：包含所有可能的状态。
2. 可达关系 (R)：定义了从一个世界到另一个世界的访问路径。
3. 赋值函数 (V)：定义命题在特定世界中的真值。

常见公理系统

• K 公理：□(P → Q) → (□P → □Q)
• T 公理：□P → P （必然性蕴含事实性，即自反性）
• 4 公理：□P → □□P （传递性）
• 5 公理：◊P → □◊P （欧几里得性）