【1】
構成的数学は古典的数学における「存在する」を「構成できる」に変えたものといえる.構成的に数学をするには,存在量化子のこういった再解釈のみならず,すべての論理結合子や量化子について,これらを含む文の証明がどのように構成されるのか指示されている必要がある.
ここでは,現代の構成的数学,つまり論理結合子と量化子のBHK解釈に基づく数学を紹介する.
【2】
構成的数学には4つのバラエティーがある.特にErrett Bishop とPer Martin-Lofによる極小的な構成可能系と見做される2つの場合を特に強調する.
【3】
そして,非公式なものではあるが,構成的逆数学の進捗を見る.この構成的逆数学は,Brouwerの扇定理などの原理を特定するための研究プログラムである.これには重要な解析的定理の証明を容易にするという利点もある.
付録として,古典数学,直観主義数学,再起数学に適用される特定の論理原理が,ビショップの構成的数学への適用を経て,ある定理の証明が容易になることを示す.
もう一つの付録として,トポロジーの構成可能的な研究について示す.
導入
数学者が何か主張するときには,それが公理でもない限り,その前に主張は正しいと証明されているものである.では,数学者がを主張するとき,彼らは何を意味するか.ここでは公式にでも非公式にでもどちらでもいいから,数学的言語の文として構文的に正しいと仮定する.普通に考えれば(と言いつつも一意的な考え方ではなくほかにも考え方があるが)「少なくとも一つの文が成り立つこと」のみならず,「どちらが成り立つか」まで決めることができる.従って,数学者はを証明により得ることができた場合にのみを主張し,そしてについては,の証明を導き出したか,の証明を導き出した場合にのみこれを主張する.
このような解釈の元でも,しかしながら,我々は深刻な問題を抱えることになる.がの否定の場合である.
を主張することは,から矛盾が導かれることである.(0=1のように.) しかし,しばしば数学者はの証明もの証明も何一つ持っていない.この状況は,Goldbach予想(GC)を見てみるだけでわかる:
(GC)
すべての2以上の整数は二つの素数の和で書くことができる.
これは長らく証明も反証もされないままである,我々はの自然な決定可能性の解釈の下で,「頑固な楽観主義者だけが排中律(LEM)を信じ続けることができる」と結論せざるを得ない.
古典論理は,論理和の解釈の拡大によってこれを回避している.つまりをとして解釈する.言い換えれば,の両方が偽であることは,偽である(矛盾を導く).ひいては,これは存在の観念論的(認識の妥当性に関する考え方の一つ)解釈につながる:は. すべてのについては矛盾を導く.
数学者が築き上げてきた,大きくそして一見難攻不落に見える古典数学の大構造物は,物理学や社会科学,生物科学などの(現在進行形で増えている)を支えるものだが,上記のような論理和や存在性に関する解釈の上に成り立っているものである.
この拡大解釈は代償を伴う.最初の自然な解釈から抜け出し,理想的なものを無制限に使うことで得られる数学は,一般に計算機モデル(例えば再起函数理論)の内で解釈することができない.
この点は,よく考えられた次の命題の例により説明される.
証明はが有理数ならとし,そうでないならば,を考えるというものである.この証明では,が有理数か無理数かわかっていないから,どちらのの組がが有理数となる組なのか特定できない.
これはまさに,最初に説明した論理和の拡大解釈,(排中律,LEM)そのものである.
もう一つの解釈の違いを説明する例を挙げる.
実数全体の集合に関する次の文を考える:
ここで,はとなる有理数を見つけることができることを意味する.自然な計算機的解釈では,任意の実数に対してかかどちらかを教えてくれる手順をもっていることをいう.しかしながら,計算機は有限の有利近似により実数を扱うことしかできない.ここでunderflowの問題が出てくる.これは十分小さな数が0とコンピュータに認識されてしまうことである.結局,の決定手続きは存在し得ない.
言い換えれば,我々の自然なの計算機解釈の下でが成立することは期待できない.
別角度から検証してみる.がが二つの素数の和で書くことができるという主張とする.ここでは正整数とする.そして無限列を次で定義する.
すると,が計算機的にwell-definedな列であることは疑いようもない.つまり,を計算するためのアルゴリズムを持っていて,が素数の和であるとき,そうでないときが返される.
ここで,番目のバイナリがであるような実数を考える.
もしが計算機的解釈のもとで成り立つならば,次の2つの選択肢のどちらかを決定することができる.
(a) であり,すべてのに対してを意味する.
(b) ある正整数でとなるものを見つけられる.
後者は,に対するテストを通じて,となるを見つけることができる.したがって,計算機的解釈により,Goldbach予想の状況を決定することができる.古典的な結果の構成的証明が,Goldbach予想を証明し得ることを示している,このタイプの例(これまで未解決な主張,例えばRiemann予想も)を,我々はBrowerian例だとか,Browerian反例などと呼ぶ.(反例は通常の意味ではない.)
このGoldbach予想の用法は実に劇的であり,例えば上述の議論は我々の計算機解釈の下で,(1)が限定的なomniscienceの原理(全知の原理)(LPO))を導く:
(LPO)
すべての2値列は,すべてのについてであるか,あるでとなるものが存在するかのいずれかである.
これはいくつかの理由から,非構成的原理と見做されている.第一にそれ自身の再帰的解釈であるところの:
ある再帰的アルゴリズムであって,再帰的に定義された2値列から,すべてのに対してならばを,あるについてならば1を返すものが存在する.
が古典論理であっても再起函数理論の中では偽であることが証明されている.したがって,すべての数学の再帰的解釈を許す場合,LPOの使用は叶わない.
第二に,あるモデル(Kripkeモデル)の中では,LPOが構成的に導出できないことが証明できてしまう.
論理の構成的解釈
もはや,数学の本格的な計算の開発においては,ほとんどの古典数学が依存している論理和や存在性の観念的解釈は許されないことは明白である.
構成的になにかするには,古典的解釈から自然な解釈に立ち返る必要がある:
(or) を証明するには,のいずれかの証明を持っている必要がある.
(and) を証明するにはそのいずれの証明ももっている必要がある.
(Implies) の証明は,の証明をの証明へ変換するアルゴリズムのこと.
(not) を証明するには,implies を示す必要がある.
(there exists) を証明するには,対象を構成しがなりたつことを証明する必要がある.
(for each/all) の証明は,任意の対象と,を証明するデータに適用してが成り立つことを証明するアルゴリズムのこと.
BHK解釈は(この名前は,Brouwer,Heyting,Kolmogorovらの仕事に起源がある.)はKleeneの実現可能性(realizabikity)の概念を用いて正確なものにできる.
よくある誤解として,構成的数学は矛盾による証明を省いただけの数学であるというものがある.これは正しくない.次の典型例を考える.は無理数である.これはが有理数であるという仮定から始まる.そして初等的に議論を進め,完全に構成的な形で,矛盾に至るのである.このような議論は,完全に構成的なの非有理性の証明といえる.実際,の構成的な解釈は,の仮定が矛盾を導くことである.この誤解は前述の証明を次のタイプの証明と混同することで生じる:
を仮定し,矛盾を導く.そして,が成り立つことを結論する.
これは非構成的である.
この視点を強化するために,次の形の証明を考える.
そのようなものは存在しないと仮定し,構成的な主張により矛盾に到達する.
このような証明には普通,そのようなものの存在を構成的に証明するアルゴリズム的な情報が含まれることはない.より形式的には,の構成的証明から自動的にを結論することはできない.
要約すると,を証明するには,を仮定して矛盾を導けばよい.を証明するには,を仮定して矛盾を導くだけでは,不十分である.
ここで,直観主義論理の実践に話を移そう.ある定理が性質が成り立つ対象の存在を主張するとき,我々はどのようなものを求めるか.この定理の証明には,の構成についてのアルゴリズムが骨格をなし,そしてが性質をもつことが必要なだけ計算される.ここにいくつかの定理の例を挙げる.それぞれの定理に対し.その構成的証明のために必要な非形式的な記述がなされている.
証明のために必要なこと(もの):実数に対して適用されるアルゴリズムであって,かを決定するもの.ただしこの決定に際しては,アルゴリズムはを記述するデータのみならず,が実数であるというデータも用いることもできる.
B
すべてのの非空部分集合に対して,それが上に有界(bounded above)ならば,最小の上界(a least upper bound)を持つ.
証明のために必要なこと(もの):実集合と,その元,そして上界に対して適用されるアルゴリズムであって,つぎのようなもの.
(i) 対象を計算し,が実数であることを示す.
(ii) がすべてのに対して成り立つことを示す.
(iii) 実数に対して,であってとなるものを計算する.
C
が閉区間上の連続実数値写像でならば,であって,かつとなるものが存在する.
証明のために必要なこと(もの):函数と関数の連続度,そしてとの値に対して適用されるアルゴリズムで,つぎのようなもの.
(i) 対象を計算し,がからの間の実数であることを示す.
(ii) を示す.
D
が閉区間上の連続実函数写像でならば,任意のに対してであってとなるものが存在する.
証明のために必要なこと:函数との連続度,そしての値,そして正数に対して適用されるアルゴリズムで,つぎのようなもの.
(i) 対象を計算し,がからの実数であることを示す.
(ii) を示す.
が構成的な証明を持つことを疑う理由はすでにある.(underflowのこと.これがBrowerian反例であることは前述の通り.)
の証明の要件が満たされる場合.すべての数学の主張に対して我々はの証明を適用することで,次の集合の上限の有理近似を計算することができる.
ここでエラーとすると,のときかどうかを,のとき かどうかを決定できる.最初のケースの場合,そして,ここからであり,が従う.もしならば,が従う.したがって,は排中律を導く.
しかしながら,ビショップの実数の構成的理論では,コーシー列の収束率が事前に定義されているがゆえに,構成的な最小上界原理を証明できる:
を非空部分実集合とし,上に有界とする.が最小上界を持つことと,それがupper-order locatedであることは同値.upper-order locatedとは,すべての実数に対して,はの上界であるか,あるいはであってとなるものが存在する.
加えて,次のような別の(区間演算に基づく)の構成的理論の展開についても言及する.(→Bridges & Vîță)
は古典的には同値であり,中間地の定理である.この文におけるの連続度とは,順序付けされた正数の組の集合であって,次の性質がなりたつものである.
(i) すべてのに対してでとなるものが存在する.
(ii) とに対して,.
文には異なる本質的に非構成的な原理,lesser limited principle of omniscience(LLPO)が含まれる:
(LLPO)
2値列であって高々一つがであり,その他がであるようなものは,がすべての偶数に対して成り立つか,がすべての奇数に対して成り立つ.
文はの弱い形であり,これは構成的に証明され,区間を半分にする標準的な議論を使う:
が閉区間上の連続実数値写像で,とする.が局所的に非零とする.つまりとに対してでとなるものが存在する.このとき,で.
中間地の定理の状況は構成的解析学における多くの典型的ものであり,我々は一つの古典的な定理に対していくつかの構成的バージョンを持っており,それらのいくつかが等価であることがわかる.
LPOやLLPOほど明確ではないomniscience原理がもう一つあり,それはマルコフ原理(MP)である.
(MP)
2値列に対し,もしすべての項が0であることに矛盾するなら,ある項は1である.
この原理はいくつかの古典的な命題と同値である.例えば次のように:
(i) 実数に対してが矛盾するなら,.
(ii) 実数に対してが矛盾するなら,であってとなるものが存在する.
(iii) 単射連続函数は,もしならである.
マルコフの原理は,非有界探索を表現している:
もしすべてのが0であることが矛盾を導くならば,とテストしていくことで,かならず1の項が見つかることが保証される.しかしながら,この保証は宇宙の終わりまでに見つかるという保証には及びません.構成的数学の実践者のほとんどは,完全な不信ではないにしろ,少なくとも疑いの目でマルコフ原理をとらえている.この見解は,MPが構成的に導出可能でないことを示すKripkeモデルの存在により強化されている.(→Bridges & Richman)
【1】の終わりに
次回は【2】です.
参考文献
https://plato.stanford.edu/entries/mathematics-constructive/