直観主義論理 vs 古典論理 — 排中律をめぐって
構成的にこだわる理由
初級（大学1-2年レベル）
このページの目標
古典論理と直観主義論理の分かれ目が排中律 $A \lor \neg A$ にあることを理解し、構成的証明とは何かをつかむ。証明検査カーネルが構成的にこだわる理由を知る。
1. 排中律という分岐点
古典論理では、どんな命題 $A$ についても「$A$ であるか、$A$ でないかのどちらかだ」と無条件に言える。これが排中律である。古典論理はさらに二重否定除去 $\neg\neg A \to A$ も認める。多くの数学者が当たり前に使う原理である。
排中律（law of excluded middle）：$A \lor \neg A$。
二重否定除去：$\neg\neg A \to A$。
古典論理はこれらを公理（または導出可能な定理）として持つ。直観主義論理は一般には持たない。
直観主義論理は、これらを無条件には認めない立場である。「$A$ が成り立つ」とは、$A$ の構成的な証拠を与えることだ、と考える。$A$ の証拠も $\neg A$ の証拠もまだ無い状況では、$A \lor \neg A$ を主張する根拠がない、というわけである。
2. 構成的証明
存在を主張するとき、実際にその対象を作る方法（証拠）を与える証明を構成的証明という。$\exists x\, P(x)$ を構成的に証明するには、具体的な $x$ と、それが $P$ を満たす証明を示さなければならない。$A \lor B$ を構成的に証明するには、どちらが成り立つかを指定しなければならない。
「無理数 $a, b$ で $a^b$ が有理数になるものが存在する」という有名な証明は、$\sqrt{2}^{\sqrt{2}}$ が有理数か無理数かで場合分けし、排中律でどちらかに決まると論じる。だがどちらが本当かは示さない。これは古典論理では正しい証明だが、対象を特定しないため構成的ではない。
背理法による存在証明、すなわち「存在しないと仮定すると矛盾するから存在する」という論法も、対象を作らないため一般に構成的ではない。構成的証明と背理法の関係は、既存記事 証明・構成的証明 でも具体例つきで扱っている。
3. 二重否定という橋渡し
直観主義論理は古典論理より弱いが、無関係ではない。直観主義でも $A \to \neg\neg A$ は示せる（逆 $\neg\neg A \to A$ が一般に示せない）。さらに、古典論理で証明できる命題は、二重否定を適切に挿入すれば直観主義論理に「翻訳」できる（Glivenko の定理、Gödel–Gentzen 翻訳）。古典論理は、直観主義論理に排中律を一つ足したものとして正確に位置づけられる。
4. 証明検査カーネルが構成的にこだわる理由
Curry–Howard 対応のもとで、構成的証明はプログラムに対応する。$\exists x\, P(x)$ の構成的証明からは、その $x$ を実際に計算するプログラムが取り出せる。証明がそのまま実行可能な内容を持つため、計算機による検証や数値計算との接続に向いている。
構成的にこだわるもう一つの理由は信頼の正直さである。排中律のような強い原理を暗黙に使わず、明示した公理と規則だけから導けば、「何を信頼の土台にしているか」が透明に保てる。必要なら排中律を明示的な公理として加えればよい。この「土台を正直に明示する」姿勢は、de Bruijn 基準・TCB や 構成的実数 の設計思想に直結する。
まとめ
この章のポイント
- 分かれ目は排中律 $A \lor \neg A$ と二重否定除去 $\neg\neg A \to A$
- 直観主義では「成り立つ」＝構成的な証拠を与えること
- 構成的証明は存在対象を実際に作る。背理法の存在証明は一般に非構成的
- 古典論理 ＝ 直観主義論理 ＋ 排中律（二重否定で翻訳できる）
- 構成的証明はプログラムに対応し、信頼の土台を正直に明示できる
よくある質問
直観主義論理と古典論理の違いは何か
古典論理は排中律 $A \lor \neg A$ と二重否定除去 $\neg\neg A \to A$ を無条件に認めるが、直観主義論理は一般に認めない。直観主義では「$A$ が成り立つ」とは $A$ の構成的な証拠を与えることを意味し、証拠がない状況では $A \lor \neg A$ を主張できない。証明できる命題の範囲が古典論理より狭い。
構成的証明とは何か
存在を主張するとき実際にその対象を作る方法（証拠）を与える証明である。$\exists x\,P(x)$ を構成的に証明するには具体的な $x$ とそれが $P$ を満たす証明を示す必要がある。「存在しないと仮定すると矛盾する」という背理法による存在証明は対象を作らないため一般に非構成的である。
なぜ証明検査カーネルは構成的論理にこだわるのか
構成的証明は Curry–Howard 対応でプログラムに対応し、存在証明からその対象を計算するプログラムが取り出せる。証明が実行可能な内容を持ち、計算機検証や数値計算との接続に向く。また排中律のような追加公理を避けて明示した公理だけから導くことで、何を信頼の土台にしているかを正直に保てる。