现代模态逻辑的早期发展，很大部分源于对经典逻辑中“实质蕴涵悖论”的不满。为了精准捕捉“必然的逻辑推演”这一直觉，C.I. Lewis 与 C.H. Langford 1932 年合著的 Symbolic Logic 第六章中，确立了系统 B ，这也是日后为人熟知的 S1 至 S5 系统的基石。
形式语言与算子：
- 命题变元： $p, q, r, \dots$
- 基本联结词： 否定 $\sim p$；逻辑积 $p \cdot q$（常简写为 $pq$）。
- 模态算子： 可能性 $\Diamond p$（Lewis 称之为 self-consistent，即自洽的/可能的）。
核心定义：
- 严格蕴涵 (Strict Implication): $p \prec q =_{def} \sim\Diamond(p \cdot \sim q)$ （不可能 $p$ 为真且 $q$ 为假）
- 严格等价 (Strict Equivalence): $p = q =_{def} (p \prec q) \cdot (q \prec p)$
7 条基础公理 (B1-B7)：
- B1. $pq \prec qp$ (交换律)
- B2. $pq \prec p$ (析取化简)
- B3. $p \prec pp$ (幂等律)
- B4. $(pq)r \prec p(qr)$ (结合律)
- B5. $p \prec \sim(\sim p)$ (双重否定)
- B6. $(p \prec q) \cdot (q \prec r) \prec (p \prec r)$ (传递律)
- B7. $p \cdot (p \prec q) \prec q$ (假言推理的内化)
四条推理规则 (Rules of Inference)：
- 代入规则 (Substitution): 允许用任意公式一致地替换定理中的命题变元。
- 随伴规则 (Adjunction): 若 $\vdash \alpha$ 且 $\vdash \beta$，则 $\vdash \alpha \cdot \beta$。（即已证定理的合取仍是定理）。
- 分离规则 (Modus Ponens): 若 $\vdash \alpha$ 且 $\vdash \alpha \prec \beta$，则 $\vdash \beta$。
- 严格等价替换 (Strict Equivalence Replacement): 若 $\vdash \alpha = \beta$，且 $\phi(\alpha)$ 是包含 $\alpha$ 的公式，则 $\vdash \phi(\alpha) = \phi(\beta)$。在缺乏演绎定理的早期系统中，这一规则对于深层语法归约至关重要。
要理解系统 B 的出现，必须追溯到 Lewis 对严格蕴涵的首次系统性探索，即其 1918 年的独立专著《符号逻辑概览》(A Survey of Symbolic Logic) 中。在该书的原始演算里，Lewis 将 $(p \prec q) = (\sim q \prec \sim p)$ 作为一条基本公理。 (第一本书的 $\sim$ 意思是不可能)
然而，Emil L. Post 在审视该系统时，敏锐地指出了一个致命缺陷：该公设会导致灾难性的“模态坍塌” (Modal Collapse)。Post 证明，以此为基础可以推导出 $p \prec q = p \supset q$（即严格蕴涵等同于实质蕴涵），这意味着系统中所有的模态词都可以被消除，彻底动摇了区分严格/实质蕴涵的哲学初衷。
为了挽救系统，Lewis 在随后的修订中去除了该公理中导致坍塌的一个蕴涵方向。这个经过削弱的 1918 版修订系统，在 1932 年的 Symbolic Logic 中被归档并命名为系统 A (System A)。而为了提供一个更稳固的底座，Lewis 和 Langford 在该书的第六章提出了一个平行且重新公理化的全新系统——系统 B (System B)。
虽然系统 B 成功避免了坍塌，当时的学者们对该系统的性质依然不清晰（例如，直到 1934 年 J.C.C. McKinsey 才证明了公理 B5 在特定扩展系统中实际上是多余的）。更紧迫的是，系统 B 有一个巨大的结构性问题：它缺乏处理无限模态迭代（如 $\Box p, \Box\Box p,...$）的归约法则。德国学者 Oskar Becker 就此发表了他的研究。
Oskar Becker (1889–1964) 是德国著名数学家兼哲学家，胡塞尔 (Edmund Husserl) 的追随者，并深受布劳威尔 (L.E.J. Brouwer) 直觉主义的影响。在 1930 年的划时代论文《模态逻辑》(Zur Logik der Modalitäten) 中，Becker 批评 Lewis 的系统留下了一个“一个开放的位置” (eine offene Stelle)——未能对模态算子的无穷迭代进行归约。
Becker 绝非在玩弄形式符号，他赋予了模态公理深刻的哲学与现象学内涵。为了封闭系统，他提出了三条著名的归约公理：
- 公理 4 (C10): $\sim\Diamond\sim p \prec \sim\Diamond\sim\sim\Diamond\sim p$。Becker 认为这反映了证明的自反本性：若 p 的证明状态为必然（已被证明），那么“p已被证明”这一事实本身，也是一个必然的真理。
- 公理 B (C12): $p \prec \sim\Diamond\sim\Diamond p$。Becker 明确称其为“布劳威尔公理” (Brouwersche Axiom)，它捕捉了直觉主义的直觉：如果 p 是真实的（已被证明），那么它绝不可能被推翻，即它必然是可能的。
- 公理 5 (C11): $\Diamond p \prec \sim\Diamond\sim\Diamond p$。
Becker 正确地指出，加入公理 5 (C11) 会使系统归约为 6 个模态词（即我们熟知的 S5）。但他却错误地断言：如果同时加入公理 4 和公理 B，会产生一个结构完全不同的、拥有 10 个独立模态词的演算系统 —— 十模态演算 (Zehn-Modalitäten-Kalkül)，并为此绘制了复杂的模态强度关系图。这一误判后来由一位中国学者纠正。
1929-1931年间，沈有鼎在哈佛大学师从 H.M. Sheffer。他察觉到了 Becker “十模态演算”的谬误，并在基础极为薄弱的系统 B 中给出了一套严谨的纯语法推演。
今天我们熟知，框架自反性的典范公式 ($ p \supset \Diamond p$) 在 Lewis 的系统中是可证的。但在当时的纯句法系统中，缺乏现代语义学视角的加持，要推导出这一点绝非易事。沈有鼎首先构建了以下基础：
预备推导：自反性定理的重建 (prerequisite propositions)
- $ \sim p \prec q \ \cdot\prec\ \sim q \prec p \quad $ (Prop. 12.2)
- $ p = \sim(\sim p) \quad $ (Prop. 12.3)
- $ p \ \cdot\prec\ \Diamond p \quad $ (Prop. 18.4)
- $ p \prec \Diamond p \ \cdot\prec\ p \supset \Diamond p \quad $
注：命题编号遵循 《符号逻辑》 (We follow the same propositional index numbers in Symbolic Logic)。
沈有鼎核心推演：证明 System B + C10 + C12 ⊢ C11 (S5)
$a.\ \sim\Diamond\sim p \prec \sim\Diamond\sim\sim\Diamond\sim p \quad $ (C10 / Axiom 4)
$b.\ \sim\sim\Diamond\sim\sim\Diamond\sim p \prec \Diamond\sim p \quad $ (a, Prop 12.2)
$c.\ \Diamond\Diamond\sim p \prec \Diamond\sim p \quad $ (b, Prop 12.3)
$d.\ \Diamond\Diamond \sim\sim p \prec \Diamond \sim\sim p \quad $ (c, Sub $[\sim p / p]$)
$e.\ \Diamond\Diamond p \prec \Diamond p \quad $ (d, Prop 12.3)
$a.\ p \prec \Diamond p \quad $ (Prop. 18.4)
$b.\ \Diamond p \prec \Diamond\Diamond p \quad $ (a, Sub $[\Diamond p/p]$)
$a.\ \Diamond\Diamond p \prec \Diamond p \ \cdot\ \Diamond p \prec \Diamond\Diamond p \quad $ (From 1 & 2)
$b.\ \Diamond\Diamond p = \Diamond p \quad $ (Def. Strict Equivalence)
$a.\ p \prec \Box\Diamond p \quad $ (C12 / Axiom B)
$b.\ \Diamond p \prec \Box\Diamond\Diamond p \quad $ (Sub $[\Diamond p/p]$)
根据 4 得出的公式（By the formula derived in step 4.）：$\Diamond p \prec \Box\Diamond\Diamond p$。
由于其包含了 (Since the formula contains) $\Diamond\Diamond p$，根据步骤 3 建立的严格等价替换原则 (by the equivalence established in step 3: $\Diamond\Diamond p = \Diamond p$) 进行代换，直接得出结论 (we get the final result by substitution.)：
$\Diamond p \prec \Box\Diamond p$ (C11 / Axiom 5)
至此证明：Becker 的“十模态演算”蕴含 S5！(This means Becker's Ten-modality calculus implies S5.)
除了沈有鼎，在这一时期，另外两位青年学者同样做出了奠基性的贡献：
- Mordchaj Wajsberg (1902–1942): 波兰华沙逻辑学派的杰出代表，逻辑学大师卢卡西维茨 (Jan Łukasiewicz) 的学生。他在 1933 年独立给出了 S5 系统的一个形式化基础，并在多值逻辑和模态逻辑领域做出了开创性工作。遗憾的是，他在二战的犹太人大屠杀中不幸遇害。尽管如此，他与 Lewis 保持通信并分享他的成果。
- William T. Parry (1908–1988): 美国哲学家，哈佛大学 W.H.Whitehead的学生，也是沈有鼎在哈佛深造期间的同窗挚友。Parry 敏锐地意识到，即便在 Lewis 的严格蕴涵系统中，仍存在类似“不可能命题严格蕴涵任何命题”的悖论。为此，他在 1933 年提出了著名的分析蕴涵 (Analytic Implication) 理论，要求蕴涵式的后件中的所有命题变元必须已经在前件中出现，开创了相关逻辑 (Relevance Logic) 的先河。
在 Symbolic Logic (1932) 的附录二中，Lewis 记载了沈有鼎 (Yuting Shen)、Parry 以及 Wajsberg的工作。其中也包括S5蕴含S4+B的证明。通过他们的共同工作，Lewis确定了多个今天为人熟知的模态逻辑系统关系，并最终确定了 S1 至 S5 模态系统层级。
沈有鼎等人的工作，其最伟大的历史意义在于完成了纯语法 (Syntax) 层面的彻底清理，极大地解放了后来的语义学 (Semantics) 研究。
试想，如果 Becker 的论断没有被沈有鼎的推演推翻，后来的数学家在寻找模态逻辑的数学模型时，将不得不去尝试构造一个对应所谓“十模态演算”的拓扑空间。沈有鼎明确指出 S4 + B 蕴含 S5，这意味着未来的语义提供者在给S4提供语义后，可以直接考虑 S5对应的数学结构即可。
后来 McKinsey 和 Tarski 提出了著名的拓扑代数语义：S4 的 $\Box$ 对应拓扑空间的“内部 (Interior)”，$\Diamond$ 对应“闭包 (Closure)”。虽然当时的数学家未必立刻意识到，一个 dense-in-itself (自身稠密) 的代数加上对应公理 B 的性质，会产生与加上公理 5 一模一样的代数结构。
S4 拓扑语义直观演示 (Kuratowski 操作)
当前状态：原始集合 $p$
📊 AWPL 学术报告
本版块研究的基础内容已在 AWPL 上进行了汇报。您可以查看或下载当时的演示幻灯片：
7. 参考文献 (References)
- Lewis, C. I. (1918). A Survey of Symbolic Logic. Berkeley: University of California Press.
- Becker, O. (1930). Zur Logik der Modalitäten. Jahrbuch für Philosophie und phänomenologische Forschung, 11, 497-548.
- Lewis, C. I., & Langford, C. H. (1932). Symbolic Logic. New York: The Century Co.
- McKinsey, J. C. C., & Tarski, A. (1944). The Algebra of Topology. Annals of Mathematics, 45(1), 141-191.
- Prior, A. N. (1956). Modality and quantification in S5. Journal of Symbolic Logic, 21, 60-62.
- Kripke, S. A. (1959). Semantic analysis of modal logic (abstract). Journal of Symbolic Logic, 24, 323-324.
- Kripke, S. A. (1963). Semantical Analysis of Modal Logic I. Zeitschrift für Mathematische Logik..., 9(5-6): 67-96.
- Lemmon, E. J. (1977). An introduction to modal logic: the Lemmon notes. Oxford: Blackwell.
- Parry, W. T. (1989). Analytic implication; its history, justification and varieties. In Directions in Relevant Logic. Dordrecht: Springer.
- Copeland, B. J. (2002). The Genesis of Possible Worlds Semantics. Journal of Philosophical Logic, 31, 99-137.
- Goldblatt, R. (2003). Mathematical modal logic: A view of its evolution. Journal of Applied Logic, 1, 309-392.
- Cresswell, M. (2019). Modal Logic before Kripke. Organon F, 26(3).
- Zhu, R. (2026). Shen Yuting in Early Modal Logic: The Axiom Interdependence of S5. AWPL Proceedings.