二重否定の除去

演繹の推論規則
命題計算
モーダスポネンスモーダストレンスモーダスポネンストレンス（英語版）連言導入簡単化選言導入選言除去選言三段論法仮言三段論法構成的ジレンマ（英語版）破壊的ジレンマ（英語版）二条件導入（英語版）二条件除去（英語版）
述語計算
普遍汎化普遍例化存在汎化存在例化
カテゴリ:推論規則
表話編歴

論理学、特に命題論理において、二重否定の除去（にじゅうひていのじょきょ、英: double negation elimination）および二重否定の導入（にじゅうひていのどうにゅう、英: double negation introduction）は、いずれも推論の種類の一つである。形式的には、いわゆる二重否定に相当する「連続した2つの否定作用素」を追加（二重否定の導入）したり削除（二重否定の除去）したりする操作を論理式に施すことである。古典論理においてはいずれも妥当な推論であるが、直観主義論理において二重否定を除去できない場合があるように、他の論理体系の下では妥当とは限らない。

例えば、

「雨が降っている」
「雨が降っていないのではない」

という2つの命題について、前者から後者を推論するのが二重否定の導入、後者から前者を推論するのが二重否定の除去である。

二重否定の除去を自然演繹の形式で表すと次のようになる。

${\dfrac {\neg \neg A}{A}}$

二重否定の導入を自然演繹の形式で表すと次のようになる。

${\dfrac {A}{\neg \neg A}}$

これらの規則はシークエントの記法を使うと次のようにも表せる。

\neg \neg A\vdash A

A\vdash \neg \neg A

これら2つの推論規則に演繹定理を適用すると、以下の2つの妥当な論理式が得られる。

\vdash \neg \neg A\rightarrow A

\vdash A\rightarrow \neg \neg A

これらは、次の1つの論理式にまとめることができる。

\vdash \neg \neg A\leftrightarrow A

双方向の含意関係は同値関係であるため、論理式内の任意の￢￢A は A に置換でき、その際にその論理式 (wff) の真理値は変化しない。

二重否定の除去は古典論理では定理だが、直観主義論理ではそうではない。直観主義論理では「この場合、雨が降っていない、のではない（It's not the case that it's not raining）」という文は「雨が降っている」よりも弱いとされる。後者は雨が降っていることを証明する必要があるが、前者は単に雨が降っているとしても矛盾しないことを証明すればよい（自然言語における緩叙法形式でもこのような区別が見られる）。二重否定の導入は直観主義論理でも定理であり、また $\neg \neg \neg A\vdash \neg A$ も成立する。