双重否定式

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

定理

[math]\displaystyle{ \vdash \lnot \lnot P \leftrightarrow P }[/math]

其对应两条变形规则，分别称为双重否定引入和双重否定消除：

[math]\displaystyle{ P \vdash \lnot\lnot P }[/math] 以及 [math]\displaystyle{ \lnot\lnot P \vdash P }[/math] 。