双重否定除去

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

「現在沒有下雨是錯的」

和

「現在正在下雨」

在語義上的等價。

形式上，雙重否定除去為

  ¬¬A
  ∴ A

形式上，雙重否定介入為

  A      
  ∴ ¬¬A

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

${\displaystyle \neg \neg A\vdash A}$,

${\displaystyle A\vdash \neg \neg A}$.

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

${\displaystyle \vdash \neg \neg A\rightarrow A}$,

${\displaystyle \vdash A\rightarrow \neg \neg A}$,

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

${\displaystyle \neg \neg A\leftrightarrow A}$.

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

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

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

另見

• 邏輯非