双重否定律（逻辑）

双重否定式(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 A }[/math] 为假，即 [math]\displaystyle{ \lnot(\lnot A) }[/math] 。隐式使用双重否定消去从而得到结论 [math]\displaystyle{ A }[/math] ；也可以认为排中律 [math]\displaystyle{ A\lor \lnot A }[/math] 在有 [math]\displaystyle{ \lnot(\lnot A) }[/math] 时通过选言三段论得到了 [math]\displaystyle{ A }[/math] 。
- 因此，反证法的有效性依赖于双重否定消去。

经典逻辑中是重要的公理或基本定理，是排中律的结果。
直觉主义逻辑中，由于双重否定消去与排中律等价，不接受否定掉否定可以直接得到原命题。需要额外的构造性证据。
- 接受双重否定引入： [math]\displaystyle{ A \rightarrow \lnot\lnot A }[/math]
- 拒绝双重否定消去： [math]\displaystyle{ \neg \neg A \rightarrow A }[/math] 不成立
多值逻辑中，真值超过两个时，双重否定式可能不成立，取决于否定算子的具体定义。
模糊逻辑中否定通常定义为真值度 [math]\displaystyle{ \neg A = 1 - A }[/math] ，此时双重否定式仍然成立：[math]\displaystyle{ \neg \neg A = A }[/math]