二重否定の除去のソースを表示

{{出典の明記| date = 2023年8月}}
{{推論規則}}
[[論理学]]、特に[[命題論理]]において、'''二重否定の除去'''（にじゅうひていのじょきょ、{{lang-en-short|double negation elimination}}）および'''二重否定の導入'''（にじゅうひていのどうにゅう、{{lang-en-short|double negation introduction}}）は、いずれも[[推論]]の種類の一つである。形式的には、いわゆる[[二重否定 (言語学)|二重否定]]に相当する「連続した2つの否定作用素」を追加（二重否定の導入）したり削除（二重否定の除去）したりする操作を[[論理式 (数学)|論理式]]に施すことである。[[古典論理]]においてはいずれも[[妥当性|妥当]]な推論であるが、[[直観主義論理]]において二重否定を除去できない場合があるように、他の論理体系の下では妥当とは限らない。

例えば、
* 「雨が降っている」
* 「雨が降っていないのではない」
という2つの[[命題]]について、前者から後者を推論するのが二重否定の導入、後者から前者を推論するのが二重否定の除去である。

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

{{Indent|<math>\dfrac{\neg\neg A}{A}</math>}}

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

{{Indent|<math>\dfrac{A}{\neg\neg A}</math>}}

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

:<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> \vdash \neg \neg A \leftrightarrow A </math>.

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

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

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

<!-- == 脚注 ==
{{脚注ヘルプ}}
{{Reflist}} -->
== 参考文献 ==
{{節スタブ}}

== 関連項目 ==
* [[否定]]
* [[二重否定 (言語学)]]

{{Mathlogic-stub}}
{{DEFAULTSORT:にしゆうひていのしよきよ}}
[[Category:古典論理]]
[[Category:推論規則]]
[[Category:命題論理の定理]]
[[Category:数学に関する記事]]