二重否定の除去

テンプレート:推論規則 二重否定の除去（にじゅうひていのじょきょ、英: Double negative elimination）は、論理学、特に命題論理における推論規則の1つである。いわゆる二重否定と等価なものを追加したり（二重否定の導入）、二重の否定作用素を削除したり（二重否定の除去）といった操作を論理式に施す。

これは、次の二つの文が等価であることに基づいている。

「雨が降っていないというのは偽である」

と

「雨が降っている」

二重否定の除去を形式的に表すと次のようになる。

  ￢￢A
  ∴ A

二重否定の導入を形式的に表すと次のようになる。

  A      
  ∴ ￢￢A

二重否定の導入（Double negative introduction）は、二重否定の除去の逆であり、命題の意味を変えずに二重否定を追加できることを意味している。

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

[math] \neg \neg A \vdash A [/math],

[math] A \vdash \neg \neg A [/math].

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

[math] \vdash \neg \neg A \rightarrow A [/math],

[math] \vdash A \rightarrow \neg \neg A [/math],

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

[math] \neg \neg A \leftrightarrow A [/math].

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

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

素朴集合論でも、補集合が同様の性質を持つ。集合 A と集合 (A^C)^C は等価である（ここで、A^C は A の補集合を意味する）。

関連項目

• 否定
• 二重否定 (言語学)