双重否定消去

双重否定消去是逻辑学中的一条推理规则，允许从 $\neg\neg A$ 推出命题 $A$；其中，$\neg\neg A$ 读作“并非非 $A$”。这条规则在经典逻辑中有效，但在直觉主义逻辑中通常不可推导。它的地位体现了两种推理方式的区别：在经典逻辑中，排除一个命题为假的可能性就能确立该命题；而在直觉主义逻辑中，这未必能提供确立命题本身所需的证据。(plato.stanford.edu)

形式表述

在自然演绎中，这条规则写作

这里的 $A$ 可以是任意公式，而不只是原子命题。在公理化表述中，对应的公理模式为

借助蕴涵引入规则和肯定前件式，这条规则与上述公理模式可以相互推导。它们既适用于命题逻辑的公式，也适用于一阶逻辑的公式。在通常的直觉主义逻辑中加入不受限制的双重否定消去，就会得到经典逻辑。(suppescorpus.stanford.edu)

反向的蕴涵

称为双重否定引入，在直觉主义逻辑中有效。给定 $A$，暂时假设 $\neg A$；两者导出矛盾，因此这个临时假设被否定。于是，经典逻辑能够确立完整的等价关系 $\neg\neg A\leftrightarrow A$，而直觉主义逻辑通常只能确立引入方向的蕴涵。(leanprover.github.io)

经典解释

在经典的真值函数语义学中，否定会将真值反转。连续应用两次否定，就会恢复原来的真值。因此，真值表为 $A$ 和 $\neg\neg A$ 赋予相同的真值：

因此，$\neg\neg A\rightarrow A$ 是一个重言式。这一等价关系针对的是具有明确含义的逻辑否定，而非日常语言中所有看似双重否定的表达。不同的逻辑系统可以赋予否定不同的性质，因此，经典真值表论证并不能确立这条规则在所有系统中的有效性。(plato.stanford.edu)

与排中律及矛盾的关系

以直觉主义逻辑为基础，不受限制的双重否定消去与排中律等价，后者为

要从排中律推导双重否定消去，可以假设 $\neg\neg A$，然后分情况推理。在 $A$ 成立的情况下，结论直接成立。在 $\neg A$ 成立的情况下，假设 $\neg\neg A$ 导出矛盾，再由爆炸原理推出 $A$。反过来，直觉主义推理能够证明 $\neg\neg(A\lor\neg A)$，随后应用双重否定消去便可得到排中律。(leanprover.github.io)

这条规则也使经典反证法成立。如果假设 $\neg A$ 导出假命题，那么解除该假设便可确立 $\neg\neg A$。双重否定消去提供了最后一步，从而得到 $A$。这必须与证明否定命题区分开来：从假设 $A$ 导出矛盾并得出 $\neg A$，本就为直觉主义逻辑所接受。经典逻辑额外允许的是，从一个已被驳倒的否定不受限制地转向肯定结论。(leanprover.github.io)

构造性解释与反模型

根据布劳威尔—海廷—柯尔莫哥洛夫解释，蕴涵的证明是一种构造，能够把其前件的证明转化为其后件的证明。否定被理解为蕴涵假命题：

因此，$\neg\neg A$ 的证明能将任何声称驳倒 $A$ 的证明转化为矛盾。这样的转化未必能给出 $A$ 的证明，尤其是在确立 $A$ 需要选择一个析取支，或给出一个存在量词的见证时。这解释了构造性观点下 $A$ 与其双重否定之间的区别。(leanprover.github.io)

可以用克里普克语义给出一个说明性的反模型。考虑两个状态 $w_0\leq w_1$，其中原子命题 $p$ 在 $w_1$ 被强制成立，但在 $w_0$ 不被强制成立。一个否定命题在某状态被强制成立，当且仅当被否定的公式在任何可达的后继状态都不被强制成立。由于 $p$ 在 $w_1$ 成立，两个状态都不强制 $\neg p$ 成立。因此，$w_0$ 强制 $\neg\neg p$ 成立，却不强制 $p$ 成立。根据直觉主义推理对于这些模型的可靠性（逻辑学），不受限制的双重否定消去在直觉主义逻辑中不可推导。这个例子展示的是语义定义，并不是把尚未确立的命题当作假命题。(cs.cmu.edu)

受限情形下的有效性与证明翻译

一般公理模式不成立，并不排除某些具体实例成立。如果 $\neg\neg A\rightarrow A$ 可被证明，就称命题 $A$ 是稳定的。如果对于某个特定命题，可以构造性地确立 $A\lor\neg A$，那么用上文相同的分类讨论论证，就能说明双重否定消去对该命题成立。否定命题也是稳定的：在直觉主义逻辑中，

因此，拒绝不受限制的双重否定消去，并不意味着拒绝一切消去两个否定符号的做法。(plato.stanford.edu)

在证明论中，双重否定翻译无需断言不受限制的双重否定消去成立，就能将经典系统与直觉主义系统联系起来。格利文科定理指出，命题公式 $A$ 在经典逻辑中可证，当且仅当 $\neg\neg A$ 在直觉主义逻辑中可证。这一简单表述不能原封不动地推广到一阶逻辑；在一阶逻辑中，需要使用更复杂的否定翻译。(plato.stanford.edu)

通过柯里—霍华德对应，这一区别也体现在类型论中：构造性的蕴涵证明具有函数的行为，而不受限制的双重否定消去需要额外的经典推理。在Lean证明助手中，经典反证法可以用 Classical.byContradiction 表达；给定假设 $h:\neg\neg A$，将它应用于 $h$，便能得到 $A$ 的证明。这使形式证明中的经典推理步骤得以明确呈现。(leanprover.github.io)