研究版块 II：沈有鼎与 C10、C12、C11 的可推导关系

Lewis 历史演算中的公理关系、现代形式重构与后续语义解释

C.I. Lewis 与 C.H. Langford 在1932年的 Symbolic Logic 第六章中给出系统 B。附录二分别使用公设组 A 与 B：A 与 Lewis 修订后的早期演算相联系，B 是第六章另行公理化的基础。本页采用系统 B 说明相关扩展，并不把后来的系统简单表述为从一个基础线性产生的序列。

形式语言与算子：

  • 命题变元： $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)$

本页使用的公理/原则 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$ (假言推理的内化)

本页只列当前说明所用的 B1–B7；完整来源还包含 B8 与 B9，本页不在缺少经审定公式的情况下转录它们。

四条推理规则 (Rules of Inference)：

  1. 代入规则 (Substitution): 允许用任意公式一致地替换定理中的命题变元。
  2. 随伴规则 (Adjunction): 若 $\vdash \alpha$ 且 $\vdash \beta$，则 $\vdash \alpha \cdot \beta$。（即已证定理的合取仍是定理）。
  3. 分离规则 (Modus Ponens): 若 $\vdash \alpha$ 且 $\vdash \alpha \prec \beta$，则 $\vdash \beta$。
  4. 严格等价替换 (Strict Equivalence Replacement): 若 $\vdash \alpha = \beta$，且 $\phi(\alpha)$ 是包含 $\alpha$ 的公式，则 $\vdash \phi(\alpha) = \phi(\beta)$。在缺乏演绎定理的早期系统中，这一规则对于深层语法归约至关重要。

Lewis 对严格蕴涵的早期系统性处理见于1918年的 A Survey of Symbolic Logic。该书原始演算把 $(p \prec q) = (\sim q \prec \sim p)$ 作为基本原则之一；在这部早期著作中，$\sim$ 的相关用法带有“不可能”的读法。

Emil L. Post 指出，该原则会导出 $p \prec q = p \supset q$，使严格蕴涵与实质蕴涵在该演算中合并，因而消去原本要表达的模态区分。

Lewis 后来删去导致这一结果的一个方向。Symbolic Logic 附录二把系统 A 与修订后的早期演算联系起来；系统 B 则是第六章另行公理化、用于相关模态扩展的基础。二者不应被描述为一个基础上的简单线性阶段。

系统 B 的性质与模态迭代的归约关系仍需研究；例如，J. C. C. McKinsey 后来讨论了 B5 在特定扩展中的冗余性，Oskar Becker 则提出了处理模态迭代的附加原则。

Oskar Becker (1889–1964) 是德国数学家、哲学家，受胡塞尔 (Edmund Husserl) 与布劳威尔 (L. E. J. Brouwer) 思想影响。在1930年的《模态逻辑》(Zur Logik der Modalitäten) 中，他把 Lewis 系统未能归约模态算子迭代称为一个“开放的位置” (eine offene Stelle)。

Becker 为这些模态原则提供了哲学与现象学解释，并提出三条归约公理：

Becker 认为加入 C11 会把模态词归约为六种；但他把同时加入 C10 与 C12 的情形描述为拥有十种独立模态词的 十模态演算 (Zehn-Modalitäten-Kalkül)。Symbolic Logic 附录二后来记载，C10 与 C12 可以推出 C11，并将这个方向归功于 Y. T. Shen（沈有鼎）。

沈有鼎于1929–1931年间在哈佛学习。Symbolic Logic 附录二明确把在相关 Lewis 基础上由 C10 与 C12 推出 C11 的方向归功于 Y. T. Shen；现有材料并不包含一份可直接认作沈有鼎逐字原稿的证明文本。

现代形式重构：下列推演依据历史演算与来源记录重建，用现代 $\Box$、$\Diamond$ 记号辅助阅读；它不是沈有鼎证明原稿的逐字转录。

现代框架语义可把 $p \supset \Diamond p$ 与自反性联系起来，但这是后来的语义解释。下列预备步骤是在 Lewis 历史演算中进行的现代重构：

预备推导：自反性定理的重建 (prerequisite propositions)

  1. $ \sim p \prec q \ \cdot\prec\ \sim q \prec p \quad $ (Prop. 12.2)
  2. $ p = \sim(\sim p) \quad $ (Prop. 12.3)
  3. $ p \ \cdot\prec\ \Diamond p \quad $ (Prop. 18.4)
  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

1. C10 的化简 (Simplification of C10): $\Diamond\Diamond p \prec \Diamond p$

$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)

2. 逆命题推导 (Converse): $\Diamond p \prec \Diamond\Diamond p$

$a.\ p \prec \Diamond p \quad $ (Prop. 18.4)

$b.\ \Diamond p \prec \Diamond\Diamond p \quad $ (a, Sub $[\Diamond p/p]$)

3. 严格等价的建立 (Equivalence): $\Diamond\Diamond p = \Diamond 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)

4. C12 的应用 (Application of C12): $\Diamond p \prec \Box\Diamond\Diamond p$

$a.\ p \prec \Box\Diamond p \quad $ (C12 / Axiom B)

$b.\ \Diamond p \prec \Box\Diamond\Diamond p \quad $ (Sub $[\Diamond p/p]$)

5. 最终归约 (Final Reduction): $\Diamond p \prec \Box\Diamond p$ (Q.E.D.)

根据 4 得出的公式（By the formula derived in step 4.）：$\Diamond p \prec \Box\Diamond\Diamond p$。
由于其包含了 (Since the formula contains) $\Diamond\Diamond p$，应用历史演算中的严格等价替换原则 (apply the historical rule for replacement by strict equivalents from step 3: $\Diamond\Diamond p = \Diamond p$)，而不是普通的文字化简 (not ordinary textual simplification)：
$\Diamond p \prec \Box\Diamond p$     (C11 / Axiom 5)

在系统 B 中，C10 与 C12 推出 C11；“4 + B → 5”只是在明确历史编号与基础之后使用的现代助记。

署名范围：附录二还记载 C11 分别推出 C10 与 C12，因此相应扩展在该基础上可互相导出；但没有证据时，不把这一反向可推导关系归功于沈有鼎。

附录二还记录了 Wajsberg 与 Parry 的相关工作；他们的贡献和时间线需要分别说明：

Symbolic Logic 附录二把沈有鼎、Parry 与 Wajsberg 的材料置于同一来源记录中，但不能据此把不同结果合并成一项“共同工作”。就沈有鼎而言，附录明确署名的是 C10 + C12 → C11；C11 → C10 与 C11 → C12 也被记载，但没有归于沈有鼎。

这一结果的数学意义在于澄清了 Lewis 相关基础上 C10、C12 与 C11 的可推导关系，并纠正 Becker 把 C10 与 C12 的组合看成独立十模态演算的判断。

现有来源记录没有证明该句法结果直接造成后来的 S4/S5 语义层级，也没有证明它使数学家避免了某种拓扑构造。沈有鼎的结果是否以及如何影响后续语义研究，仍是需要传播文献支持的历史问题。

历史上，汤璪真在1938年给出 Lewis 严格蕴涵演算的一种代数/几何或拓扑解释，McKinsey–Tarski 在1944年给出后续处理。把现代模态记号 $\Box$ 读作内部、$\Diamond$ 读作闭包，是本页帮助理解后续语义的现代说明；下图只是记号助记，不是历史模型，也不执行真实的拓扑运算。

汤璪真 1938 / TANG 1938

历史层：汤璪真的欧氏平面构造

汤璪真从带单位元的布尔环公设 A–E 出发，加入一元运算 x∞，其公设为 x∞x=x∞ 与 (xy)∞=x∞y∞。在主要几何实现中，1 是欧氏平面，布尔元素是点集，乘法是交，补集相对于 1；点属于 x∞ 当且仅当以该点为圆心的某个欧氏圆全在 x 内。因此 x∞ 对应内部，(1−x)∞ 是外部，1−x∞−(1−x)∞ 是边界，1−(1−x)∞ 是闭包。可能性定义为 ◇x=1−(1−x)∞；严格蕴涵可现代规范化为 x≺y=¬◇(x¬y)=(x⊃y)∞。这些解释属于这项特定历史构造。

汤璪真的定理 36 只涉及所表示理论 T 中的严格蕴涵及其解释中的可断言性。这一层不把他的构造改写成任意有限拓扑空间，也不把该受限方向说成完备性结果。Baylis 的同期评论指出：汤璪真没有证明 Lewis 公设反向推出全部 A–F2 代数公设。

Tang 1938Baylis 1939

现代有限模型 / MODERN FINITE MODEL

现代层：有限拓扑模型 M = (X, τ, V)

X 是非空有限点集，τ 是包含 ∅ 与 X、并且对任意并与有限交封闭的开集族，V 把原子 p、q、r 映到 X 的子集。现代记号中，[[□φ]] = Int([[φ]])，[[◇φ]] = Cl([[φ]])。

现代记号 / MODERN NOTATION

无 JavaScript 也可核查的 Sierpiński 型示例

取 X={a,b}、τ={∅,{b},{a,b}}、V(p)={b}，并选定点 b。于是 Int(V(p))={b}、Cl(V(p))={a,b}；所以 [[□p]]={b}（在 b 为真但不在整个模型处处为真），而 [[◇p]]={a,b}（在当前模型每一点都为真）。

后续定理/语义背景 / LATER THEOREM/CONTEXT

历史比较边界

McKinsey、Tarski 及后来的拓扑模态逻辑成果属于后续背景。有限模型中的一次计算只说明选定点、当前模型或明确枚举的当前有限拓扑；它不是汤璪真完备性证明，也不是所有拓扑空间上的模态有效性证明。

📊 AWPL 学术报告

本版块研究的基础内容已在 AWPL 上进行了汇报。您可以查看或下载当时的演示幻灯片：

🔗 幻灯片链接： Shen Yuting in Early Modal Logic (Slides)

7. 参考文献 (References)