双重否定律（逻辑）

双重否定式
术语名称	双重否定式
英语名称	double negation
别名	DN

双重否定式(double negation, DN)是命题逻辑定理之一，指一个命题两次否定等价于其自身。

定理

永真式 [math]\displaystyle{ \vDash \lnot \lnot P \leftrightarrow P }[/math] 称为双重否定式(double negation)，简写为 DN 。

两个方向对应的永真式也分别称为：

• 双重否定引入： [math]\displaystyle{ \vDash P \rightarrow \lnot\lnot P }[/math] ，或 [math]\displaystyle{ P\vDash \lnot\lnot P }[/math] 。
• 双重否定消除： [math]\displaystyle{ \vDash \lnot\lnot P\rightarrow P }[/math] ，或 [math]\displaystyle{ \lnot\lnot P \vDash P }[/math] 。

意义

• 在自然演绎系统中，双重否定式的两条定理对应两条变形规则：
  • 双重否定引入： [math]\displaystyle{ P\vdash \lnot\lnot P }[/math] 。
  • 双重否定消除： [math]\displaystyle{ \lnot\lnot P \vdash P }[/math] 。
• 在 Hilbert 系统中，双重否定式常作为重要定理出现。
• 双重否定式与排中律密切相关：
  • 在古典逻辑中，双重否定消去等价于排中律；
  • 若一个逻辑系统接受排中律，则其必然接受双重否定式。
• 双重否定式是反证法的基础：
  • 反证法通过证明 [math]\displaystyle{ \lnot A }[/math] 导致矛盾得出 [math]\displaystyle{ \lnot(\lnot A) }[/math] 时，得到结论 [math]\displaystyle{ A }[/math] ，这里隐式使用了双重否定消去；
  • 因此，反证法的有效性依赖于双重否定消去。

非经典逻辑中的情况

• 直觉主义逻辑
  • 接受双重否定引入：[math]\displaystyle{ A \rightarrow \neg \neg A }[/math]
  • 拒绝双重否定消去：[math]\displaystyle{ \neg \neg A \rightarrow A }[/math]不成立
  • 认为双重否定消去需要额外的构造性证据
• 多值逻辑
  • 真值超过两个时，双重否定式可能不成立，取决于否定算子的具体定义
• 模糊逻辑
  • 否定通常定义为[math]\displaystyle{ \neg A = 1 - A }[/math] ，此时双重否定式仍然成立：[math]\displaystyle{ \neg \neg A = A }[/math]