建設的な証明

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

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

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

構成的証明は、証明された数学的アルゴリズムを定義するものとして考えることができます。この考え方は、構成的論理のBrouwer-Heyting-Kolmogorov 解釈、証明とプログラム間のCurry-Howard 対応、およびPer Martin-Löfの直観主義型理論やThierry CoquandとGérard Huetの構成計算などの論理システムで探求されています。

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

これまで考えられていた問題を解決するために非構成的証明が初めて使用されたのは、ヒルベルトの零定理とヒルベルトの基底定理であると思われる。哲学的な観点からは、前者は明確に指定されたオブジェクトの存在を意味するため、特に興味深い。

零点定理は次のように述べられる。もしn個の不定 元における多項式が複素係数を持ち、共通の複素零点を持たない場合、${\displaystyle f_{1},\ldots ,f_{k}}$${\displaystyle g_{1},\ldots ,g_{k}}$

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

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

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

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

まず、素数は無限にあるという定理を考えてみましょう。ユークリッドの証明は構成的です。しかし、ユークリッドの証明を簡略化する一般的な方法は、定理の主張に反して、素数は有限個しかなく、その場合は最大の素数nが存在すると仮定します。次に、数n ! + 1 (1 + 最初のn個の数の積) を考えます。この数は素数であるか、その素因数がすべてnより大きいかのどちらかです。特定の素数を確立することなく、元の公理に反して、 nより大きい数が存在することが証明されます。

ここで、「無理数 が存在し、 は有理数である」という定理を考えてみましょう。この定理は、構成的証明と非構成的証明の両方を使用して証明できます。 ${\displaystyle a}$${\displaystyle b}$${\displaystyle a^{b}}$

1953年にドヴ・ジャーデンが行った以下の証明は、少なくとも1970年以降、非構成的証明の例として広く使われてきた。^{[4] [5]}

CURIOSA
339. 無理数の無理指数乗が有理数である可能性があることの簡単な証明。は有理数か無理数のどちらかです。 有理数であれば、私たちの主張は証明されます。 無理数であれば、私たちの主張は証明されます。      Dov Jarden Jerusalem
${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$${\displaystyle ({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2}$

もう少し詳しく説明すると:

• は無理数、2 は有理数であることを思い出してください。数 を考えてみましょう。これは有理数か無理数のいずれかです。${\displaystyle {\sqrt {2}}}$ ${\displaystyle q={\sqrt {2}}^{\sqrt {2}}}$
• が有理数である場合、定理は真であり、 とは両方とも です。${\displaystyle q}$${\displaystyle a}$${\displaystyle b}$${\displaystyle {\sqrt {2}}}$
• が無理数であれば、 でありであるとき、定理は真である。なぜなら、${\displaystyle q}$${\displaystyle a}$${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$${\displaystyle b}$${\displaystyle {\sqrt {2}}}$

${\displaystyle \left({\sqrt {2}}^{\sqrt {2}}\right)^{\sqrt {2}}={\sqrt {2}}^{({\sqrt {2}}\cdot {\sqrt {2}})}={\sqrt {2}}^{2}=2.}$

本質的に、この証明は非構成的です。なぜなら、この証明は「q は有理数か無理数のいずれかである」という命題に依存しているからです。これは排中律の例であり、構成的証明では有効ではありません。非構成的証明は例aとb を構築するのではなく、単にいくつかの可能性 (この場合は、互いに排他的な 2 つの可能性) を示し、そのうちの 1 つが目的の例を生み出すはずであることを示しますが、どれが目的の例であるか は示しません。

結局のところ、ゲルフォン・シュナイダー定理により は無理数ですが、この事実は非構成的証明の正しさとは無関係です。 ${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$

無理数の無理指数乗は有理数になる可能性があるという定理の 構成的証明は、次のような実際の例で示されます。

${\displaystyle a={\sqrt {2}}\,,\quad b=\log _{2}9\,,\quad a^{b}=3\,.}$

2 の平方根は無理数で、3 は有理数です。も無理数です。 に等しい場合、対数の性質により、9 ^{n は2 m}に等しくなりますが、前者は奇数で、後者は偶数です。 ${\displaystyle \log_{2}9}$${\displaystyle m \over n}$

より実質的な例はグラフマイナー定理である。この定理の帰結は、グラフのマイナーがいずれも「禁制マイナー」の有限集合に属していない場合に限り、そのグラフをトーラス上に描くことができるということである。しかし、この有限集合の存在の証明は構成的ではなく、禁制マイナーは実際には指定されていない。^[6]これらはまだ不明である。

構成的数学では、古典数学と同様に、反例を挙げることで命題を反証できる。しかし、その命題が非構成的であることを示すために、ブローワーの反例を挙げることも可能である。 ^[7]この種の反例は、その命題が非構成的であることが知られている何らかの原理を暗示していることを示す。その命題が構成的に証明できない何らかの原理を暗示していることが構成的に証明できる場合、その命題自体は構成的に証明できない。

たとえば、特定の命題が排中律を暗示することが示される場合があります。このタイプの Brouwerian 反例の例はDiaconescu の定理です。これは、選択公理全体が構成的集合論のシステムでは非構成的であることを示しています。これは、選択公理がそのようなシステムでは排中律を暗示するためです。構成的逆数学の分野では、さまざまな原理を「非構成性の程度」で分類し、それらが排中律のさまざまな断片と同等であることを示すことで、この考え方をさらに発展させています。

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

${\displaystyle a(n)={\begin{cases}(1/2)^{n}&{\mbox{区間 }}[4,n]{\mbox{ 内の偶数の自然数が 2 つの素数の和である場合}},\\(1/2)^{k}&{\mbox{}}k{\mbox{ が区間 }}[4,n]{\mbox{ 内の最小の偶数の自然数であり、2 つの素数の和ではない場合}}\end{cases}}}$

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

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

• 構成主義（数学の哲学）
• Errett Bishop - 『構成的分析の基礎』の著者。
• 存在定理 § 「純粋な」存在の結果
• 非構成的アルゴリズムの存在証明
• 確率的方法

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