建設的証明

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

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

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

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

歴史的な例

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

非構成的証明がこれまで考えられてきた問題を解くために初めて用いられたのは、ヒルベルトの零定理とヒルベルトの基底定理であると思われる。哲学的な観点から見ると、前者は明確に規定された対象の存在を示唆する点で特に興味深い。

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

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

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

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

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

例

非構成的証明

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

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

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

CURIOSA 339.無理数の無理指数乗が有理数となる可能性があることの簡単な証明。は有理数か無理数のどちらかです。もし有理数であれば、私たちの主張は証明されます。もし無理数であれば、私たちの主張は証明されます。ドヴ・ジャーデン・エルサレム ${\sqrt {2}}^{\sqrt {2}}$ $({\sqrt {2}}^{\sqrt {2}})^{\sqrt {2}}=2$

もう少し詳しく説明します。

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

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

この証明の本質は、非構成的であるということです。なぜなら、この証明は「qは有理数か無理数かのどちらかである」という命題、つまり排中律の例に依拠しており、これは構成的証明においては成立しないからです。非構成的証明は、例aとbを構成するのではなく、単に複数の可能性（この場合は互いに排反する2つの可能性）を提示し、そのうちの1つが必ず目的の例を生み出すことを示しているだけで、どの可能性が望ましい例を生み出すかは示していません。

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

構成的証明

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

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

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

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

ブローワー反例

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

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

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

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」という構成的証明が存在する場合、これは（前者の場合）ゴールドバッハ予想の構成的証明が存在する、あるいは（後者の場合）ゴールドバッハ予想が誤りであることの構成的証明が存在することを意味します。そのような証明が知られていないため、引用された文にも構成的証明は知られていないはずです。しかし、ゴールドバッハ予想に構成的証明が存在する可能性は十分にあります（現時点ではそれが存在するかどうかは不明です）。その場合、引用された文にも、現時点では未知ではあるものの、構成的証明が存在することになります。弱い反例の主な実用的な用途は、問題の「困難さ」を特定することです。例えば、先ほど示した反例は、引用された文が「少なくともゴールドバッハ予想と同じくらい証明が難しい」ことを示しています。この種の弱い反例は、全知の限定的な原理と関連していることが多い。

参照

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

参考文献

^ Bridges, Douglas; Palmgren, Erik (2018)、「Constructive Mathematics」、Zalta, Edward N. (ed.)、The Stanford Encyclopedia of Philosophy (Summer 2018 ed.)、Metaphysics Research Lab、Stanford University 、 2019年10月25日閲覧。
^マクラティ、コリン（2008年4月15日）。『乱された円：数学と物語の相互作用』第4章「ヒルベルトの神学とその不満論：近代数学の起源神話」。アポストロス・K.・ドキシアデス（1953-）、バリー・マズール（ 1953- ）著。プリンストン：プリンストン大学出版局。doi ：10.1515/9781400842681.105。ISBN 9781400842681. OCLC 775873004 . S2CID 170826113 .
^ヘルマン、グレーテ (1926)。「Die Frage der endlich vielen Schritte in der Theorie der Polynomideale: Unter Benutzung nachgelassener Sätze von K. Hentzelt」。Mathematische Annalen (ドイツ語)。95 (1): 736–788。土井: 10.1007/BF01206635。ISSN 0025-5831。S2CID 115897210。
^ J. Roger Hindley、「非構成性の例としてのルート2の証明」、未発表論文、2014年9月、全文は Wayback Machineで2014年10月23日にアーカイブされています。
^ Dov Jarden、「無理数の無理数乗が有理数となる可能性があることの簡単な証明」、 Curiosa No. 339 in Scripta Mathematica 19 :229 (1953)
^ Fellows, Michael R.; Langston, Michael A. (1988-06-01). 「多項式時間決定可能性を証明するための非構成的ツール」(PDF) . Journal of the ACM . 35 (3): 727– 739. doi : 10.1145/44483.44491 . S2CID 16587284 .
^マンデルカーン, マーク (1989). 「ブラウワーの反例」.数学マガジン. 62 (1): 3– 27. doi : 10.2307/2689939 . ISSN 0025-570X . JSTOR 2689939 .
^ AS Troelstra,直観主義の原理, 数学講義ノート95, 1969年, p. 102
^ Mark van Atten, 2015, 「弱い反例」、スタンフォード数学百科事典

さらに読む

J. フランクリン、A. ダウド (2011) 『数学の証明：入門』キューブックス、ISBN 0-646-54509-4、第4章
ハーディ, GH &ライト, EM (1979) 『数論入門（第5版）』オックスフォード大学出版局. ISBN 0-19-853171-0
Anne Sjerp TroelstraおよびDirk van Dalen (1988)「数学における構成主義: 第 1 巻」エルゼビアサイエンス。ISBN 978-0-444-70506-8

外部リンク

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

[1] Bridges, Douglas; Palmgren, Erik (2018)、「Constructive Mathematics」、Zalta, Edward N. (ed.)、The Stanford Encyclopedia of Philosophy (Summer 2018 ed.)、Metaphysics Research Lab、Stanford University 、 2019年10月25日閲覧。

[2] マクラティ、コリン（2008年4月15日）。『乱された円：数学と物語の相互作用』第4章「ヒルベルトの神学とその不満論：近代数学の起源神話」。アポストロス・K.・ドキシアデス（1953-）、バリー・マズール（ 1953- ）著。プリンストン：プリンストン大学出版局。doi ：10.1515/9781400842681.105。ISBN 9781400842681. OCLC 775873004 . S2CID 170826113 .

[3] ヘルマン、グレーテ (1926)。「Die Frage der endlich vielen Schritte in der Theorie der Polynomideale: Unter Benutzung nachgelassener Sätze von K. Hentzelt」。Mathematische Annalen (ドイツ語)。95 (1): 736–788。土井: 10.1007/BF01206635。ISSN 0025-5831。S2CID 115897210。

[4] J. Roger Hindley、「非構成性の例としてのルート2の証明」、未発表論文、2014年9月、全文は Wayback Machineで2014年10月23日にアーカイブされています。

[5] Dov Jarden、「無理数の無理数乗が有理数となる可能性があることの簡単な証明」、 Curiosa No. 339 in Scripta Mathematica 19 :229 (1953)

[6] Fellows, Michael R.; Langston, Michael A. (1988-06-01). 「多項式時間決定可能性を証明するための非構成的ツール」(PDF) . Journal of the ACM . 35 (3): 727– 739. doi : 10.1145/44483.44491 . S2CID 16587284 .

[7] マンデルカーン, マーク (1989). 「ブラウワーの反例」.数学マガジン. 62 (1): 3– 27. doi : 10.2307/2689939 . ISSN 0025-570X . JSTOR 2689939 .

[8] AS Troelstra,直観主義の原理, 数学講義ノート95, 1969年, p. 102

[9] Mark van Atten, 2015, 「弱い反例」、スタンフォード数学百科事典

[ 1 ]

[ 2 ]

[

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]