🔢 mathematics

Classical Logic as Intuitionistic Logic with Duality

本文提出了一种针对经典逻辑的新颖证明论语义，该语义通过在原始对偶文字而非原子命题上进行运算，扩展了直觉主义逻辑，从而证明了经典逻辑可以被理解为由一个推导编码的对偶原则所补充的直觉主义逻辑。

原作者： Alexander V. Gheorghiu, Yll Buzoku

发布于 2026-06-03

📖 1 分钟阅读🧠 深度阅读

原作者： Alexander V. Gheorghiu, Yll Buzoku

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心思想：逻辑是一场“是”与“否”的游戏

想象一下，你正试图向一位朋友解释逻辑是如何运作的。通常，我们认为逻辑是一套用于确定什么是真（True）、什么是**假（False）**的规则。

这篇论文提出了一种看待它的不同方式。与其问“这个陈述是真的吗？”，作者们问的是：“我能否断言这个？”（说“是”）或者“我能否否定这个？”（说“否”）。

他们的核心口号是：

经典逻辑 = 直觉主义逻辑 + 对偶性 (Duality)

用通俗的话说：他们认为，我们数学和科学中使用的复杂“经典逻辑”，实际上只是更简单的“直觉主义逻辑”（这种逻辑对证明的要求非常严格）加上一条特殊的规则——即从一开始就将“是”和“否”视为两个相等且相反的力量。

登场人物

为了理解他们的论点，我们需要认识这个故事中的三位主要角色：

内容 (Content，即“是什么”)： 这是原始的想法，比如“音乐会很棒”。
力量 (Force，即“如何做”)： 这是你表达想法的方式。你可以断言 (Assert) 它（说“音乐会很棒！”），或者否定 (Deny) 它（说“音乐会很糟！”）。
公式 (Formula，即“结构”)： 这是由这些想法构建的复杂句子，比如“如果音乐会很棒，那么我会留下”。

旧方式 vs. 新方式

旧方式（传统逻辑）：
想象你有一个电灯开关。它要么是开 (ON)（真），要么是关 (OFF)（假）。

如果你想说“不”，你只需把开关拨到“关”。
在这种观点下，“否定”某事仅仅是“断言其相反面”。
问题在于： 作者认为这太简单了。它假设在我们开始争论之前，答案已经是“是”或“否”了。这就像是在你还没插上插头之前，就假设电灯开关一定能工作一样。

新方式（作者的方法）：
想象两个人在对话，一个“说‘是’的人”和一个“说‘否’的人”。

他们不是从电灯开关开始的。他们从文字 (Literals) 开始。
文字 (Literal) 是一种基本的言语行为。
- 肯定文字 (Positive Literal)： “我断言：音乐会很棒。”
- 否定文字 (Negative Literal)： “我否定：音乐会很棒”（这相当于说“音乐会很糟”）。
关键点： 这两者并不是由彼此定义的。你不能说“否定只是断言的反面”。它们是两个独立的、原始的工具，就像锤子和螺丝刀。你不能通过把锤子翻过来就把它变成螺丝刀；它们是本质上不同的工具。

“对偶性”的秘诀

论文指出，要从简单的逻辑（直觉主义逻辑）过渡到复杂的逻辑（经典逻辑），你只需要添加一条关于这些“是”与“否”工具如何在最底层（原子层面）进行交互的规则。

他们引入了关于这些基本工具的两条简单规则：

“排斥”规则 (The "Exclusion" Rule)： 你不能在同一时间对同一件事既说“是”又说“否”。如果你试图同时断言“音乐会很棒”并且否定“音乐会很棒”，系统就会崩溃（你会得到一个矛盾，或称之为“荒谬”）。
“分类讨论”规则 (The "Case Analysis" Rule)： 如果无论你假设“是”还是假设“否”，都能证明一个结果，那么你就不需要知道哪一个是真的，就可以得出该结果。你可以直接说：“无论哪种情况都已得到证明。”

类比：
想象你正试图进入一家夜总会。

直觉主义逻辑： 你需要一份特定的邀请函（证明）才能进去。如果你没有，你就进不去。
经典逻辑（带有对偶性）： 如果你有一张“是”通行证，或者有一张“否”通行证（这张“否”通行证的作用是“不，我不是被拒之门外”），你就可以进去。
作者展示了，如果你拥有这两张通行证（断言和否定）以及上述两条规则，你就可以构建出整个经典逻辑的结构，而无需预先假设一个“真/假”的世界存在。

为什么这很重要（“这与我有什么关系？”）

作者正在解决一个哲学谜题。

谜题： 如果我们是“反现实主义者”（即相信真理是我们通过证明来“构建”出来的，而不是漂浮在天空中现成存在的东西），我们如何使用假设一切非真即假的“经典逻辑”？
解决方案： 通过将“是”和“否”视为两个平等的、原始的言语行为，他们证明了经典逻辑并不需要假设预先存在一个“真/假”的世界。它只需要关于我们如何使用“是”和“否”进行辩论的规则。

技术成就

这篇论文在数学上完成了一件非常聪明的事情：

他们采用了标准的、简单的直觉主义逻辑规则（这些规则已经被充分理解）。
他们仅在最底层的“文字 (Literals)”层面添加了“对偶性”规则（排斥和分类讨论）。
他们证明了这种简单的添加创造了完整且强大的经典逻辑系统。

他们称之为基底扩展语义学 (Base-Extension Semantics)。可以这样理解建筑过程：

直觉主义逻辑是地基和框架。
经典逻辑是同样的房子，但底部安装了一个特殊的“对偶门”。
一旦安装了这个门，整个房子运作起来就会有所不同，允许进行所有复杂的经典数学推理，但它是使用直觉主义逻辑那些简单的、构造性的砖块建造而成的。

总结

论文认为：经典逻辑并非一种神秘的、预先存在的真理。它只是直觉主义逻辑（基于证明的逻辑）加上一个简单的共识——即“是”和“否”是两个平等的、相反的力量，我们可以利用它们来构建复杂的论证。

通过将“否定”视为一种原始工具，而非仅仅是“断言其相反面”，他们为理解经典推理如何运作提供了一种全新的、构造性的视角，而无需去相信一个神奇的“真/假”宇宙。

技术摘要：作为具有对偶性的直觉主义逻辑的经典逻辑

1. 问题所在
本文探讨了意义理论中的一个基础性挑战：如何为经典逻辑提供一种遵循反实在论（构造主义）原则、且不预设二值性或超越验证之真理（verification-transcendent truth）原则的证明论语义学（P-tS）。虽然 Sandqvist 已成功为直觉主义逻辑（IPL）开发了基底扩展语义学（B-eS），并为经典逻辑（CPL）开发了一个版本，但仍存在局限性。Sandqvist 的 CPL 语义学受限于特定的联结词（最初为 $\to, \bot, \forall$ ），并且依赖于一个涉及条归纳法（bar induction）的技术极其复杂的完备性证明。此外，现有方法往往难以构造性地处理完整的命题语言（包括 $\lor$ 和 $\exists$ ）。作者旨在通过为完整的经典命题逻辑提供一种 B-eS 来解决这一问题，该语义学保持了初等且构造性的完备性证明，从而回应了 Dummett 关于如何将经典推理与反实在论意义相调和的挑战。

2. 方法论与哲学框架
作者提出了一个双边主义框架，将经典逻辑概念化为“直觉主义逻辑 + 对偶性”。这种方法背离了传统观点，通过在原子层面区分内容与言语行为力（illocutionary force），同时将复杂公式视为逻辑语法结构而非本身带有行为力的命题。

文字（Literals）作为命题： 该系统引入了“文字”（ $L$ ）作为断言（assertion）与否定的唯一对象。一个内容 $c$ 与一个行为力配对，形成正向文字（ $c^+$ ，断言）或负向文字（ $c^-$ ，否定）。至关重要的是，对偶性是原初的： $c^+$ 和 $c^-$ 是独立的原子言语行为，而非通过否定（ $\neg$ ）定义。
逻辑语法结构： 复杂公式（例如 $\phi \land \psi$ ）不是被断言或否定的命题，而是组织推理的结构。因此，双边区分（断言 vs. 否定）仅限于原子层面（文字）。
推论对偶性： 经典性并非通过添加真值语义来恢复，而是通过在原子层面引入两个和谐的推论原则（遵循 Negri 和 von Plato）：
1. 排除（EXC1）： 断言与否定同一内容会导致荒谬（ $l, l^\perp \vdash \bot$ ）。
2. 分类讨论（EXC2）： 如果一个结论从一个断言及其对偶否定中都能导出，则该结论直接成立（ $l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$ ）。

3. 技术发展

自然演绎系统 ( $NK^\pm$ )： 作者定义了一个自然演绎系统，该系统由标准的直觉主义规则（$NJ$）加上原子对偶规则（EXC1 和 EXC2）组成。该系统将文字视为基础，通过标准联结词构建复杂公式。
基底扩展语义学 (B-eS)：
- 基底 ( $B$ )： 基底是一个原子规则集合（文字之间的推论关系）。
- 可推导性 ( $\vdash_B$ )： 基底中的可推导性通过归纳定义。它包括标准结构规则（自反性、应用性）以及两个新增的子句（exc1, exc2），用以在文字层面强制执行对偶性。
- 支持 ( $\Vdash_B$ )： 公式之有效性根据公式结构进行归纳定义。至关重要的是，联结词（ $\to, \land, \lor$ ）的支持子句与 Sandqvist 的直觉主义定义完全相同。经典的特性完全由定义可推导性中的对偶子句所承载，而非由复杂公式的支持子句承载。
- 有效性 ( $\Gamma \Vdash \phi$ )： 若一个公式在所有基底中都被支持，则称该公式是有效的。

4. 关键结果

可靠性 (定理 5.1)： 该系统是可靠的：如果 $\Gamma \vdash_{NK^\pm} \phi$ ，则 $\Gamma \Vdash \phi$ 。证明过程通过对推导进行归纳，展示了经典规则（EXC1, EXC2）如何保持支持性。
完备性 (定理 6.2)： 该系统是完备的：如果 $\Gamma \Vdash \phi$ $Γ ⊩ ϕ$ ，则 $\Gamma \vdash_{NK^\pm} \phi$ $Γ ⊢_{N K^{\pm}} ϕ$ 。
- 证明过程改编自 Sandqvist 对直觉主义逻辑的初等方法。
- 它利用了一个从序列子公式中构造的“模拟基底”（ $\mathcal{N}$ ）。
- 一个“平坦化”（flattening）算子将复杂公式映射到模拟基底内的原子文字。
- “自然化”（Naturalizing）引理证明了模拟基底中的可推导性可以转换回 $NK^\pm$ 中的可推导性。
- 与以往的方法不同，此证明处理了完整的命题语言（包括 $\lor$ ），并依赖于初等数学资源，避免了条归纳法或规范模型。

5. 重要性与主张
本文声称提供了一种新型的经典逻辑证明论语义学，该语义学：

统一了 IPL 与 CPL： 它表明经典逻辑可以被理解为在直觉主义逻辑基础上，在原子层面补充了原初的对偶性原则。
尊重反实在论： 通过避开真值与二值性，并使用构造性完备性证明，它为经典逻辑提供了一个真正的反实在论基础，回应了 Dummett 的基础性挑战。
简化技术复杂度： 通过将双边主义限制在文字层面并将复杂公式视为结构，作者实现了一个具有“显著初等特征”的完备性证明，其水平可与 Sandqvist 对直觉主义逻辑的工作相媲美，克服了以往经典 B-eS 尝试中的技术困难。
提供了一种替代模型论的方案： 作者将这项工作定位为模型论语义学以及现有依赖模型论概念（如 Makinson 或 Eckhardt 和 Pym 的工作）的 P-tS 方法的替代方案，旨在建立一种纯粹的推论主义经典逻辑说明。

文章总结道，这一框架为类似于直觉主义逻辑在 P-tS 传统中已建立的系统性处理方式，为系统性处理经典逻辑开辟了可能性。