双重否定除去

命题逻辑里,双重否定除去(或双重否定介入)此一推理规则允许导入(双重否定介入)或除去(双重否定除去)一对否定来导出等价的公式。这是基于如

“现在没有下雨是错的”

“现在正在下雨”

在语义上的等价。

形式上,双重否定除去为

  ¬¬A
  ∴ A

形式上,双重否定介入为

  A      
  ∴ ¬¬A

这两个规则可以重述如下(以相继式的形式):

,
.

应用演绎定理于这两个推理规则中可产生一对有效的条件公式:

,
,

两者可以结合成单一个双条件公式

.

因为双条件是一个等价关系,任一于合式公式中的~~A都可以由A所取代,而不改变此合式公式的真值。

双重否定除去是经典逻辑里的一个定理,但不是直觉逻辑里的。因为直觉逻辑在结构上的偏好,“不是没有正在下雨”此一陈述比“正在下雨”要弱。后者需要有下雨的证明,而前者只需要证明下雨不会矛盾。(此一差别亦出现在自然语言的反叙法之中。)

集合论里也有符合此性质的补集否定运算:集合A和集合 (AC)C(这里的AC表A的补集)是相同的。

另见

编辑