双重否定除去

在命題邏輯裡，雙重否定除去（或雙重否定介入）此一推理規則允許導入（雙重否定介入）或除去（雙重否定除去）一對否定來導出等價的公式。這是基於如

:「現在沒有下雨是錯的」

和

:「現在正在下雨」

在語義上的等價。

形式上，雙重否定除去為

:¬¬A

:∴ A

形式上，雙重否定介入為

:AA     
:∴ ¬¬A

這兩個規則可以重述如下（以相繼式的形式）：

: \neg \neg A \vdash A ,

: A \vdash \neg \neg A .

應用演繹定理於這兩個推理規則中可產生一對有效的條件公式：

: \vdash \neg \neg A \rightarrow A ,

: \vdash A \rightarrow \neg \neg A ,

兩者可以結合成單一個雙條件公式

: \neg \neg A \leftrightarrow A .

因為雙條件是一個等價關係，任一於合式公式中的~~A都可以由A所取代，而不改變此合式公式的真值。

雙重否定除去是經典邏輯裡的一個定理，但不是直覺邏輯裡的。因為直覺邏輯在結構上的偏好，「不是沒有正在下雨」此一陳述比「正在下雨」要弱。後者需要有下雨的證明，而前者只需要證明下雨不會矛盾。（此一差別亦出現在自然語言的反敘法之中。）

在集合論裡也有符合此性質的補集否定運算：集合A和集合 (AC)C（這裡的AC表A的補集）是相同的。

另見
*邏輯非