Glivenko's theorems from an ecumenical perspective

技术摘要：从普世视角看格利文科定理

问题陈述
本文探讨了经典逻辑（CL）与直觉主义逻辑（IL）之间的基础关系，特别是重新审视格利文科定理。这些定理确立了：如果一个公式在经典逻辑中可证，则其双重否定在直觉主义逻辑中可证；如果一个否定公式在经典逻辑中可证，则它在直觉主义逻辑中也可证。虽然这些结果在独立逻辑系统的背景下已被充分理解，但本文研究了这些关系如何在普世系统中显现。普世系统是统一的框架，其中经典逻辑和直觉主义逻辑和平共存而不相互消解，通常通过区分算子（例如经典析取与直觉主义析取）或通过标记公式以指示其逻辑性质来实现。核心问题在于确定当经典推理与直觉主义推理被整合到单一演绎系统中时，格利文科类型的结果如何转化，并分析两种主要普世方法之间的差异：即“推论主义”方法（区分算子）和“普遍主义”方法（通过标签区分公式）。

方法论
作者采用基于自然演绎系统的证明论分析。他们考察了三个具体的普世框架：

1. NE（Prawitz 系统）：一种推论主义方法，其中经典逻辑学家和直觉主义逻辑学家共享中性算子（合取、全称量词、否定、谬误），但拥有非中性算子（蕴涵、析取、存在量词）的不同版本。
2. ECI（Barroso-Nascimento 系统）：一种普遍主义方法，使用单一算子集，但公式被标记上常量 $c$（例如 $A^c$）以表示经典行为。该系统建立在直觉主义自然演绎之上，并增加了针对该标签的引入规则（$I_C$）和消去规则（$E_C$）。
3. NEK（受 Krauss 启发的系统）：Prawitz 系统的一个变体，包含经典合取（$\land_c$）和经典全称量词（$\forall_c$），基于 Krauss 未发表的工作。

方法论包括：

• 在这些系统内部定义格利文科类型的定理（将经典算子/公式与其直觉主义对应物联系起来）。
• 构建推导以证明这些内部关系。
• 定义翻译函数（$t_{ECI}$ 和 $t_{NEK}$）以在系统之间映射公式。
• 研究这些系统的演绎等价性，特别是命题片段与涉及全称量化的一阶片段之间的差异。

主要贡献与结果

1. NE 中的内部格利文科定理：
   作者证明，在 Prawitz 的系统（NE）中，由于存在不同的算子，内部存在一种“格利文科类型”的关系。对于任何主算子为经典的公式 $C$，有 $C \vdash_{NE} \neg\neg C^*$，其中 $C^*$ 是将经典算子替换为其直觉主义对应物后的公式。这适用于经典析取（$\lor_c$）、蕴涵（$\to_c$）和存在量化（$\exists_c$）。对于否定公式也有相应的结果：$\neg C \vdash_{NE} \neg C^*$。

2. ECI 中格利文科结果的平凡性：
   在 ECI 系统中，经典公式 $A^c$ 与其直觉主义对应物之间的关系在结构上是平凡的。该系统的规则立即得出 $A^c \vdash_{ECI} \neg\neg A$。因此，将 $A^c$ 映射为 $\neg\neg A$ 的翻译 $t_{ECI}$ 将 ECI 中的归一化问题简化为直觉主义逻辑的问题。作者表明，虽然这种翻译适用于命题逻辑，但它掩盖了经典推理在推导中的具体位置，除非仔细重构推导以追踪所得公式的“经典性质”。

3. 经典合取与 NEK 的情况：
   本文介绍了 NEK，它在 Prawitz 系统的基础上增加了经典合取（$\land_c$）。作者证明了 $\land_c$ 满足内部格利文科定理（$B \land_c C \vdash_{NEK} \neg\neg(B \land_i C)$）。他们还表明，在命题片段（或不包含全称量词的一阶逻辑）中，NEK 和 ECI 是演绎等价的。这种等价性是通过翻译 $t_{NEK}$ 建立的，该翻译将 NEK 中的经典算子映射为 ECI 中的标记公式。

4. 全称量化带来的分歧：
   一个关键结果是，当引入全称量化时，NEK 和 ECI 之间的演绎等价性失效。

   • 在 NEK 中，经典全称量词 $\forall_c$ 是通过与直觉主义逻辑和谐的规则定义的。然而，内部格利文科定理对 $\forall_c$ 失效：$\vdash_{NEK} \forall_c x A(x)$ 并不蕴含 $\vdash_{NEK} \neg\neg \forall_i x A(x)$。
   • 在 ECI 中，标记公式 $(\forall x A(x))^c$ 的表现则不同。由于系统的规则，$(\forall x A(x))^c \vdash_{ECI} \neg\neg \forall x A(x)$ 成立。
   • 作者解释了这种差异：在 NEK 中，$\forall_c x A(x)$ 被解释为 $\neg \exists x \neg A(x)$，而在 ECI 中，$(\forall x A(x))^c$ 实际上被解释为 $\neg\neg \forall x A(x)$。这两者在直觉主义逻辑中并不等价。本文认为，ECI 中全称公式的格利文科结果的“平凡性”源于标签 $c$ 强制了一种双重否定解释，这种解释与推论主义方法中经典全称量词的语义行为不一致。

意义与主张
本文主张，普世视角提供了对经典推理与直觉主义推理之间相互作用的更深入理解。通过比较“推论主义”（NE/NEK）和“普遍主义”（ECI）方法，作者突显了一个微妙但重要的概念差异：

• 推论主义系统（Prawitz/Krauss）通过为经典算子提供不同的引入和消去规则，直接改变连接词的含义。
• 普遍主义系统（ECI）改变证明的层级，通过标签 $c$ 赋予直觉主义逻辑经典证明手段，从而间接改变算子的含义。

作者得出结论，虽然这些方法在命题逻辑中是等价的，但在存在全称量化的情况下它们会产生分歧。这种分歧表明，普世框架的选择不仅仅是符号偏好问题，而是会影响量词的逻辑行为。本文提出，普世视角有助于精确定位经典推理的必要性所在，并阐明经典原则与直觉主义原则可以在不相互消解的情况下共存，前提是系统的构建需关注这些不同的推论原则。