双重否定除去

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

「現在沒有下雨是錯的」

「現在正在下雨」

在語義上的等價。

形式上,雙重否定除去為

  ¬¬A
  ∴ A

形式上,雙重否定介入為

  A      
  ∴ ¬¬A

這兩個規則可以重述如下(以相繼式的形式):

,
.

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

,
,

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

.

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

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

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

另見