構成的証明
From Wikipedia, the free encyclopedia
構成的証明（こうせいてきしょうめい、英: constructive proof）とは、数学的命題の証明において、命題の真を示すだけでなく、その証明から対象の構成法、計算手続き、または証明対象を具体的に取り出しうる型の証明をいう。とくに構成的数学および直観主義論理の文脈では、存在命題の証明は単なる矛盾導出ではなく、該当する対象を与える構成を含むものと解される。したがって、構成的証明は排中律や存在命題に対する非構成的背理法を許容する古典的証明概念と対比される。[1][2]
構成的証明の思想的背景は20世紀初頭のライツェン・エヒベルトゥス・ヤン・ブラウワーの直観主義にあるが、その後アーレント・ハイティングによる形式化、証明論および再帰理論における研究を経て、今日では数学基礎論のみならず、型理論、カリー＝ハワード同型対応、定理証明支援系などとも深く結びついている。現代の標準的説明では、構成的証明はブラウワー＝ハイティング＝コルモゴロフ解釈（BHK解釈）により特徴づけられ、命題の証明をその命題の構成的内容を担う対象として理解する。[3][4][5]
古典数学では、存在命題 \(\exists x\,P(x)\) を示すために、\(\neg\exists x\,P(x)\) を仮定して矛盾を導くという方法が広く用いられる。これに対して構成的証明では、一般にそのような間接的議論のみでは十分でなく、実際に \(P(x)\) を満たす対象 \(x\) を与えるか、あるいはそれを得る方法を明示することが求められる。構成的数学の標準的立場では、「存在する」とは「構成できる」と読むべきであるとされる。[1][6]
ただし、構成的証明は単に具体例を一つ挙げる証明に尽きるものではない。より本質的には、証明が証明対象または計算内容を持つという見方に特徴がある。命題の証明は、その命題を成り立たせる構成を与えるものであり、論理結合子や量化子の意味も、そのような構成の与え方を通じて理解される。[1][5]
論理学的基礎
BHK解釈
構成的証明の標準的説明は、BHK解釈によって与えられる。これは、論理結合子および量化子を真理値論的にではなく、「その命題の証明が何であるか」という観点から説明するものである。現代構成的数学の概説では、構成的推論の意味論的背景としてBHK解釈が中心的位置を占める。[1][2]
BHK解釈の下では、命題の証明はおおむね次のように理解される。
- \(A \land B\) の証明は、\(A\) の証明と \(B\) の証明の組である。
- \(A \rightarrow B\) の証明は、\(A\) の任意の証明から \(B\) の証明を与える変換である。
- \(A \lor B\) の証明は、\(A\) または \(B\) のいずれが成り立つかを指定し、その側の証明を与えることである。
- \(\exists x\,P(x)\) の証明は、具体的な対象 \(a\) と \(P(a)\) の証明を与えることである。
- \(\forall x\,P(x)\) の証明は、任意の \(a\) に対して \(P(a)\) の証明を与える方法である。[1][4]
直観主義論理との関係
構成的証明の形式的背景を与える代表的体系が直観主義論理である。直観主義論理は、ブラウワーの直観主義数学から抽象された一般的推論原理を体系化したものであり、ロシア構成主義やビショップ流構成的数学にも共通する論理的基盤とみなされる。[7]
直観主義論理では、古典論理で一般に採用される排中律
- \(A \lor \neg A\)
および二重否定除去
- \(\neg\neg A \rightarrow A\)
は一般には定理とならない。これは、これらの原理がBHK解釈の下では一様な構成を与えないためである。[7][5]
もっとも、構成的証明が間接証明一般を排除するわけではない。否定 \(\neg A\) は \(A \rightarrow \bot\) と解されるため、否定命題に関する証明や、矛盾導出に基づく特定の議論は構成的文脈でも許容される。しかし、存在命題を単に矛盾から導出するだけでは、通常は構成的証明とは見なされない。[1]
選言性質と存在性質
構成的証明が内容を持つことは、証明論的には選言性質（disjunction property）および存在性質（existence property）によって表現される。概略的には、閉論理式 \(A \lor B\) が証明可能であれば、その証明から \(A\) と \(B\) のいずれが成り立つかが取り出せること、また閉論理式 \(\exists x\,A(x)\) が証明可能であれば、具体的な証人を与える項が得られることを意味する。これらは、構成的証明が選言情報や存在証人を内包するという特徴を形式的に述べたものである。[7][5]
とくにハイティング算術などの体系では、算術的存在命題の証明から具体的な数値証人を取り出しうるという意味で、数的存在性質が議論される。[3]
歴史
構成的証明の思想的源流はブラウワーの直観主義にある。ブラウワーは、数学を人間精神の構成活動として理解し、数学的対象の存在はその構成可能性に基づくと考えた。[3]
ブラウワー自身は形式化に対して批判的であったが、ハイティングはその立場を形式論理として整備し、直観主義論理を確立した。さらに、ゲンツェンの自然演繹とシークエント計算、クライニーの実現可能性理論などを通じて、構成的証明は証明論・意味論・再帰理論の各方面から研究されるようになった。[7][8]
20世紀後半には、エレット・ビショップが『Foundations of Constructive Analysis』において、古典解析学の大きな部分を構成的に再構成する計画を示した。ビショップ流構成主義は、ブラウワー流直観主義に比べて哲学的主張を抑制し、通常の数学実践に近いかたちで構成性を維持しようとするものであり、現代構成的数学の代表的潮流の一つとされる。[6][1]
さらに、ペール・マルティン＝レーフは構成的証明を型付き項として扱う直観主義型理論を提示し、証明と計算の対応を前景化した。この方向はのちの定理証明支援系の理論的基盤となった。[4][9]
例
非構成的証明の例
古典数学でしばしば挙げられる例として、「無理数 \(a,b\) が存在して \(a^b\) が有理数である」という命題の証明がある。\(\sqrt{2}^{\sqrt{2}}\) が有理数であれば \(a=b=\sqrt{2}\) とすればよく、そうでなければ \(a=\sqrt{2}^{\sqrt{2}},\,b=\sqrt{2}\) とおくことで \(a^b=2\) が得られる。この議論は古典的には正しいが、途中でどちらの場合が成り立つかを決定していないため、構成的観点では非構成的証明の典型例とされる。[2]
構成的証明の例
これに対し、「偶数 \(n\) に対して \(\exists k\in\mathbb{Z}\,(n=2k)\)」を示すとき、\(k=n/2\) を具体的に与える証明は構成的である。また、「任意の自然数 \(x\) に対して \(\exists y\,(y=x+1)\)」という命題の証明は、\(x\) を受け取って \(x+1\) を返す一様な方法を与えるものと理解される。構成的数学では、このように量化の証明が関数的・一様的手続きとして与えられることが重視される。[1]
構成的数学における位置づけ
構成的数学では、定理の意味はその証明の与える構成内容と密接に結びついている。このため、古典数学では同値とみなされる命題であっても、構成的文脈では情報量の差が本質的意義を持つことがある。たとえば、ある解が存在することと、その解を与える方法が存在することとは、古典的にはしばしば区別されないが、構成的数学では後者こそが前者の実質的内容とみなされる。[1][10]
また、古典解析学の定理の中には、構成的にはそのままでは成立しないものや、追加条件のもとで再定式化を要するものがある。構成的数学の概説では、中間値の定理などが、古典版の単一の命題としてではなく、構成的内容に応じて複数の異なる主張に分解される例として挙げられている。[1]