構成的証明

数学において、構成的証明とは、数学的対象の存在を、対象を作成する方法、あるいは対象を作成する方法を提供することによって証明する手法である。これは、特定の種類の対象の存在を例を示さずに証明する非構成的証明（存在証明または純粋存在定理とも呼ばれる）とは対照的である。後述するより強い概念との混同を避けるため、このような構成的証明は、有効証明と呼ばれることもある。

構成的証明は、構成的数学において有効な証明というより強い概念を指す場合もある。 構成主義は、明示的に構築されていない対象の存在を伴うすべての証明方法を拒否する数学哲学である。これは特に、排中律、無限公理、選択公理の使用を排除する。構成主義はまた、いくつかの用語に異なる意味をもたらす（例えば、「または」という用語は、古典数学よりも構成的数学においてより強い意味を持つ）。^{[ 1 ]}

非構成的な証明の中には、ある命題が偽であれば矛盾が生じ、結果としてその命題は真でなければならないことを示すものがある（背理法）。しかし、直観主義を含むいくつかの構成的数学の分野では、爆発原理（ex falso quodlibet）が受け入れられている。

構成的証明は、認証された数学的アルゴリズムを定義するものと見なすことができる。この考え方は、構成的論理のブロウワー・ヘイティング・コルモゴロフ解釈、証明とプログラム間のカリー・ハワード対応、ペル・マルティン・レーフの直観主義型理論やティエリー・コカンとジェラール・ユエの構成計算などの論理体系において探求されている。

19世紀末まで、数学的証明は基本的にすべて構成的であった。非構成的な構成が初めて登場したのは、ゲオルク・カントールの無限集合論と実数の形式的な定義である。

以前に検討された問題を解決するために非構成的証明が初めて用いられたのは、ヒルベルトのヌルシュテルンザッツとヒルベルトの基底定理であると思われる。哲学的観点から見ると、前者は明確に定義された対象の存在を暗示するため、特に興味深い。

Nullstellensatzは次のように述べることができます。${\displaystyle f_{1},\ldots ,f_{k}}$は、複素係数を持つn個の不定元に関する多項式であり、共通の複素零点を持たない。このとき、多項式は存在する。${\displaystyle g_{1},\ldots ,g_{k}}$そのため

${\displaystyle f_{1}g_{1}+\ldots +f_{k}g_{k}=1.}$

このような非構成的な存在定理は当時の数学者たちにとって非常に驚きであり、そのうちの一人であるポール・ゴードンは「これは数学ではなく、神学だ」と書いた。^{[ 2 ]}

25年後、グレーテ・ヘルマンは計算のためのアルゴリズムを提供した。${\displaystyle g_{1},\ldots ,g_{k},}$これは、彼女がヒルベルトの結果を用いたため、強い意味での構成的証明ではない。彼女は、もし${\displaystyle g_{1},\ldots ,g_{k}}$存在する場合、以下の度数で見つけることができます $2^2^n$[ ^{3 ]​}

これはアルゴリズムを提供する。なぜなら、問題は線形方程式系の解法に帰着し、有限個の係数を未知数として考慮するからである。${\displaystyle g_{i}.}$

構成的数学では、古典数学と同様に、反例を与えることで命題を反証することができます。しかし、ブロウワーの反例を与えることで、その命題が非構成的であることを示すことも可能です。 ^{[ 7 ]}この種の反例は、その命題が非構成的であることが知られている何らかの原理を含意していることを示しています。もし、その命題が構成的に証明できない何らかの原理を含意していることが構成的に証明できるならば、その命題自体も構成的に証明することはできません。

例えば、ある特定の命題が排中律を含意することが示される場合がある。この種のブロウワー的反例の一例として、ディアコネスクの定理が挙げられる。この定理は、選択公理がそのような体系において排中律を含意するため、完全な選択公理は構成的ではないことを示している。構成的逆数学の分野では、様々な原理が排中律の様々な断片と等価であることを示すことで、それらの原理が「どれほど非構成的か」という観点から分類し、この考え方をさらに発展させている。

ブロワーはまた、「弱い」反例も提示した。^{[ 8 ]}しかし、そのような反例は命題を否定するものではなく、現時点ではその命題の構成的証明が知られていないことを示すにすぎない。弱い反例の1つは、 4より大きいすべての偶数の自然数が2つの素数の和であるかどうかを問うゴールドバッハ予想のような、数学の未解決問題を取り上げることから始まる。次のように有理数の数列a ( n ) を定義する。 ^{[ 9 ]}

${\displaystyle a(n)={\begin{cases}(1/2)^{n}&{\mbox{if every even natural number in the interval }}[4,n]{\mbox{ is the sum of two primes}},\\(1/2)^{k}&{\mbox{if }}k{\mbox{ is the least even natural number in the interval }}[4,n]{\mbox{ which is not the sum of two primes}}\end{cases}}}$

各nに対して、 a ( n )の値は網羅的な探索によって決定できるため、a は構成的に明確に定義された数列です。さらに、a は収束率が一定のコーシー数列であるため、構成的数学における実数の通常の扱いに従って、a はある実数αに収束します。

実数αに関するいくつかの事実は構成的に証明できます。しかし、構成的数学における言葉の意味が異なるため、「α = 0 またはα ≠ 0」という構成的証明が存在する場合、これは (前者の場合) ゴールドバッハ予想の構成的証明が存在するか、(後者の場合) ゴールドバッハ予想が偽であるという構成的証明が存在することを意味します。そのような証明は知られていないため、引用された命題にも既知の構成的証明はありません。しかし、ゴールドバッハ予想に構成的証明が存在する可能性は十分にあります (現時点ではそれが存在するかどうかはわかりません)。その場合、引用された命題にも構成的証明が存在することになりますが、現時点ではそれは不明です。弱い反例の主な実用的な用途は、問題の「難しさ」を特定することです。たとえば、先ほど示した反例は、引用された命題がゴールドバッハ予想と「少なくとも証明するのが難しい」ことを示しています。このような弱い反例は、しばしば全知の限定原理に関連している。

• 構成主義（数学の哲学）
• エレット・ビショップ- 『構成的分析の基礎』の著者。
• 存在定理 §  「純粋」存在結果
• 非構成的アルゴリズムの存在証明
• 確率的方法

• マーク・ヴァン・アッテン著『弱い反例』（スタンフォード哲学百科事典）