查看“︁双重否定除去”︁的源代码

{{unreferenced|time=2016-04-11T10:34:40+00:00}}
在[[命題邏輯]]裡，'''雙重否定除去'''（或'''雙重否定介入'''）此一推理規則允許導入（雙重否定介入）或除去（雙重否定除去）一對否定來導出等價的公式。這是基於如

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

和

:「現在正在下雨」

在語義上的等價。

形式上，雙重否定除去為

   <u>¬¬A</u>
   ∴ A

形式上，雙重否定介入為

   <u>A      </u>
   ∴ ¬¬A

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

:<math> \neg \neg A \vdash A </math>,

:<math> A \vdash \neg \neg A </math>.

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

:<math> \vdash \neg \neg A \rightarrow A </math>,

:<math> \vdash A \rightarrow \neg \neg A </math>,

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

:<math> \neg \neg A \leftrightarrow A </math>.

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

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

在[[樸素集合論|集合論]]裡也有符合此性質的[[補集]]否定運算：集合A和集合 (A<sup>C</sup>)<sup>C</sup>（這裡的A<sup>C</sup>表A的補集）是相同的。

==另見==

*[[邏輯非]]

{{logic-stub}}
[[Category:邏輯]]
[[Category:推理規則]]