爆発律

古典論理や直観主義論理、および類似の形式体系において、爆発律（ばくはつりつ、Principle of explosion）テンプレート:Efnテンプレート:Efnとは、矛盾から任意の命題が証明できるという原理である。 つまり、矛盾からは、任意の主張（およびその否定）が演繹されるということであり、これは deductive explosion としても知られている。

この原理は、12世紀のフランスの哲学者テンプレート:仮リンクによって初めて証明された。 爆発律は、形式体系が無矛盾でないということが、破滅的な結果をもたらすことを意味する。任意の命題が証明できるということは、真偽の概念がもはや無意味なものとなってしまうからである。

20世紀初頭には、数学基礎論においてラッセルのパラドックスなどの矛盾が発見され、これによって数学的構造そのものが脅かされることとなった。このような矛盾を取り除くために、ゴットロープ・フレーゲ、エルンスト・ツェルメロ、アドルフ・フレンケル、トアルフ・スコーレムといった数学者が集合論の再構築に尽力し、現代数学の基礎となるツェルメロ＝フレンケル集合論が確立された。

爆発律の一例として、「全てのレモンは黄色である」と「全てのレモンが黄色であるわけではない」という矛盾する二つの文を考え、その両方が真であると仮定する。すると、例えば「ユニコーンは実在する」という命題は、以下のような論法によって証明される:

1. 仮定より、全てのレモンが黄色であるわけではない。
2. 仮定より、全てのレモンは黄色である。
3. よって、「全てのレモンは黄色である または ユニコーンは実在する」という文も真である。なぜならば、この文の前半部分（「全てのレモンは黄色である」）は、既に仮定されているからである。
4. しかし、「全てのレモンが黄色であるわけではない」という文も（仮定より）また真であるから、3の文の前半部分は偽である。したがって、3の文全体が真であるとすれば、文の後半部分が真でなくてはならない。つまり、ユニコーンは実在する（このような推論は選言三段論法として知られている）。
5. 同様の手順により、ユニコーンが実在しないことも証明できる（よって、「ユニコーンは実在すると同時に実在しない」という矛盾も導かれる）。これは、任意の論理式に対して適用できるため、真であるような命題が爆発的に増加する。

爆発律がもたらす問題への別のアプローチとして、矛盾許容論理と呼ばれる別種の論理を考案した数学者もいる。これは、他の（全ての）文の真理値に影響を与えることなく、いくつかの矛盾する命題を証明できるようにするものである。

記号的表現

記号論理学では、爆発律は次のような記法で表現される: テンプレート:Indent

証明

以下に示すのは、記号論理学を用いた爆発律の形式的証明であるLewis argument である。

ステップ	命題	説明
1	$P\wedge \mathrm{\neg }P$	前提テンプレート:Efn
2	$P$	論理積の消去 (1)
3	$\mathrm{\neg }P$	論理積の消去 (1)
4	$P\vee Q$	論理和の導入 (2)
5	$Q$	選言三段論法 (4,3)

この証明は、C・I・ルイスによって発表され、彼の名にちなんで命名されたものの、中世の論理学者には既に知られていることであった。

これは、$P$が「全てのレモンは黄色である」を表し、$Q$が「ユニコーンは実在する」を表すとすれば、先述の非形式的な議論を記号によって表現したものとなる。

まず、(1)「全てのレモンは黄色」であり、(2)「全てのレモンが黄色であるわけではない」、と仮定する。全てのレモンは黄色であるという命題から、(3)「全てのレモンが黄色であるか、ユニコーンが実在するかのどちらかである」と推論する。しかし、これと「全てのレモンが黄色であるわけではない」という事実から、選言三段論法によって、(4)「ユニコーンが実在する」ことが推論される。

意味論的論証

爆発律について、モデル理論の観点から論証することもできる。

文$P$が、文の集合$\mathrm{\Gamma }$の論理的帰結となるのは、$\mathrm{\Gamma }$の任意のモデルが$P$のモデルでもある場合に限られる。しかし、矛盾集合$(P\wedge \mathrm{\neg }P)$のモデルは存在しない。テンプレート:仮リンク（ましてや）、$(P\wedge \mathrm{\neg }P)$のモデルであって$Q$のモデルでないようなものは存在しない。ゆえに、vacuously（空虚なことに）、$(P\wedge \mathrm{\neg }P)$の全てのモデルは$Q$のモデルである。したがって、$Q$は$(P\wedge \mathrm{\neg }P)$の論理的帰結である。

矛盾許容論理

矛盾許容論理においては、テンプレート:仮リンクの関係を作り出すような特別な演算子を許容するものがある。

モデル理論の立場においては、$\{\varphi ,\mathrm{\neg }\varphi \}$のモデルが存在しないという古典的な仮定を否定し、そのようなモデルが存在するような意味論的体系を考える場合がある。あるいは、命題が真と偽のいずれか一方のみに分類できるという古典的な仮定を否定することもある。

証明論の立場においては、爆発律を導くために必要となる選言三段論法、論理和の導入、背理法といった推論の妥当性を否定することもある。

超数学的な意味

超数学的には、爆発律を採用する体系において、もし矛盾⊥（あるいはこれと等価な$\varphi \wedge \mathrm{\neg }\varphi$）を証明するような理論が導かれたとしたら、全ての命題が定理となり、真と偽を区別することが不可能となってしまう。したがって、その理論は無価値なものと見なされる。

換言すれば、爆発律の存在は、古典論理における無矛盾律の重要性を示す論拠となる。なぜなら、無矛盾律が成り立たないのだとしたら、真偽に関する全ての主張が意味をなさなくなるからである。

爆発律を採用しない体系における証明能力の低減については、最小論理において議論されている。

関連項目

• テンプレート:仮リンク – クラヴィウスの法則。$(\mathrm{\neg }P\to P)\to P$
• 真矛盾主義 – 「真なる矛盾が存在する」という哲学上の立場
• 排中律 – 任意の命題は真または偽である
• 無矛盾律 – 真かつ偽である命題は存在しない
• 矛盾許容論理 – 矛盾を特別な方法で扱う論理体系
• 実質含意のパラドックス – 爆発律から導かれる一種のパラドックス
• 背理法 – 仮定から矛盾を導くことで、その仮定の誤りを結論する手法
• テンプレート:仮リンク – 「（矛盾を含む）全ての命題が真である」という論理学上の立場