0

Constructive Mathematics【1】

207
0

【1】
構成的数学は古典的数学における「存在する」を「構成できる」に変えたものといえる.構成的に数学をするには,存在量化子のこういった再解釈のみならず,すべての論理結合子や量化子について,これらを含む文の証明がどのように構成されるのか指示されている必要がある.

ここでは,現代の構成的数学,つまり論理結合子と量化子のBHK解釈に基づく数学を紹介する.

【2】
構成的数学には4つのバラエティーがある.特にErrett Bishop とPer Martin-Lofによる極小的な構成可能系と見做される2つの場合を特に強調する.

【3】
そして,非公式なものではあるが,構成的逆数学の進捗を見る.この構成的逆数学は,Brouwerの扇定理などの原理を特定するための研究プログラムである.これには重要な解析的定理の証明を容易にするという利点もある.

付録として,古典数学,直観主義数学,再起数学に適用される特定の論理原理が,ビショップの構成的数学への適用を経て,ある定理の証明が容易になることを示す.

もう一つの付録として,トポロジーの構成可能的な研究について示す.

導入

数学者が何か主張するときには,それが公理でもない限り,その前に主張は正しいと証明されているものである.では,数学者がPQを主張するとき,彼らは何を意味するか.ここでP,Qは公式にでも非公式にでもどちらでもいいから,数学的言語の文として構文的に正しいと仮定する.普通に考えれば(と言いつつも一意的な考え方ではなくほかにも考え方があるが)「少なくとも一つの文P,Qが成り立つこと」のみならず,「どちらが成り立つか」まで決めることができる.従って,数学者はPを証明により得ることができた場合にのみPを主張し,そしてPQについては,Pの証明を導き出したか,Qの証明を導き出した場合にのみこれPQを主張する.

このような解釈の元でも,しかしながら,我々は深刻な問題を抱えることになる.QPの否定の場合である.

¬Pを主張することは,Pから矛盾が導かれることである.(0=1のように.) しかし,しばしば数学者はPの証明も¬Pの証明も何一つ持っていない.この状況は,Goldbach予想(GC)を見てみるだけでわかる:

(GC)

すべての2以上の整数は二つの素数の和で書くことができる.

これは長らく証明も反証もされないままである,我々はPQの自然な決定可能性の解釈の下で,「頑固な楽観主義者だけが排中律(LEM)を信じ続けることができる」と結論せざるを得ない.

(LEM)

すべてのPに対して,Pか,¬Pが成り立つ.

古典論理は,論理和の解釈の拡大によってこれを回避している.つまりPQ¬(¬P¬Q))として解釈する.言い換えれば,P,Qの両方が偽であることは,偽である(矛盾を導く).ひいては,これは存在の観念論的(認識の妥当性に関する考え方の一つ)解釈につながる:xP(x)¬x¬P(x). すべてのxについてP(x)は矛盾を導く.

数学者が築き上げてきた,大きくそして一見難攻不落に見える古典数学の大構造物は,物理学や社会科学,生物科学などの(現在進行形で増えている)を支えるものだが,上記のような論理和や存在性に関する解釈の上に成り立っているものである.

この拡大解釈は代償を伴う.最初の自然な解釈から抜け出し,理想的なものを無制限に使うことで得られる数学は,一般に計算機モデル(例えば再起函数理論)の内で解釈することができない.

この点は,よく考えられた次の命題の例により説明される.

ある無理数a,bであってabが有理数となるものが存在する.

証明は22が有理数ならa=b=2とし,そうでないならば,a=22,b=2を考えるというものである.この証明では,22が有理数か無理数かわかっていないから,どちらの(a,b)の組がabが有理数となる組なのか特定できない.
これはまさに,最初に説明した論理和の拡大解釈,(排中律,LEM)そのものである.

もう一つの解釈の違いを説明する例を挙げる.
実数全体の集合Rに関する次の文を考える:

(1)

xR(x=0x0),

ここで,x00<r<|x|となる有理数を見つけることができることを意味する.自然な計算機的解釈では,任意の実数xに対してx=0x0かどちらかを教えてくれる手順をもっていることをいう.しかしながら,計算機は有限の有利近似により実数を扱うことしかできない.ここでunderflowの問題が出てくる.これは十分小さな数が0とコンピュータに認識されてしまうことである.結局,(1)の決定手続きは存在し得ない.

言い換えれば,我々の自然な,の計算機解釈の下で(1)が成立することは期待できない.

別角度から検証してみる.G(n)2n+2が二つの素数の和で書くことができるという主張とする.ここでnは正整数とする.そして無限列a=(a1,a2,)を次で定義する.
an={0 G(k)kn1 ¬G(k)kn
すると,aが計算機的にwell-definedな列であることは疑いようもない.つまり,anを計算するためのアルゴリズムを持っていて,4,6,2n+2が素数の和であるときan=0,そうでないときan=1が返される.

ここで,n番目のバイナリがanであるような実数xを考える.
x=(0.a1a2)2=21a1+22a2=n=12nan.

もし(1)が計算機的解釈のもとで成り立つならば,次の2つの選択肢のどちらかを決定することができる.

(a) x=21a1+22a2+=0であり,すべてのnに対してan=0を意味する.
(b) ある正整数N21a1+>2Nとなるものを見つけられる.

後者は,a1,aNに対するテストを通じて,an=1となるnNを見つけることができる.したがって,計算機的解釈により,Goldbach予想の状況を決定することができる.古典的な結果Pの構成的証明が,Goldbach予想を証明し得ることを示している,このタイプの例P(これまで未解決な主張,例えばRiemann予想も)を,我々はBrowerian例だとか,Browerian反例などと呼ぶ.(反例は通常の意味ではない.)

このGoldbach予想の用法は実に劇的であり,例えば上述の議論は我々の計算機解釈の下で,(1)が限定的なomniscienceの原理(全知の原理)(LPO))を導く:

(LPO)

すべての2値列(a1,a2,)は,すべてのnについてan=0であるか,あるnan=1となるものが存在するかのいずれかである.

これはいくつかの理由から,非構成的原理と見做されている.第一にそれ自身の再帰的解釈であるところの:

ある再帰的アルゴリズムであって,再帰的に定義された2値列(a1,a2)から,すべてのnに対してan=0ならば0を,あるnについてan=1ならば1を返すものが存在する.

が古典論理であっても再起函数理論の中では偽であることが証明されている.したがって,すべての数学の再帰的解釈を許す場合,LPOの使用は叶わない.

第二に,あるモデル(Kripkeモデル)の中では,LPOが構成的に導出できないことが証明できてしまう.

論理の構成的解釈

もはや,数学の本格的な計算の開発においては,ほとんどの古典数学が依存している論理和や存在性の観念的解釈は許されないことは明白である.

構成的になにかするには,古典的解釈から自然な解釈に立ち返る必要がある:

(or)  PQを証明するには,P,Qのいずれかの証明を持っている必要がある.
(and)  PQを証明するにはそのいずれの証明ももっている必要がある.
(Implies)  PQの証明は,Pの証明をQの証明へ変換するアルゴリズムのこと.
¬(not)  ¬Pを証明するには,Pimplies 0=1を示す必要がある.
(there exists)  xP(x)を証明するには,対象xを構成しP(x)がなりたつことを証明する必要がある.
(for each/all)  xSP(x)の証明は,任意の対象xと,xSを証明するデータに適用してP(x)が成り立つことを証明するアルゴリズムのこと.

BHK解釈は(この名前は,Brouwer,Heyting,Kolmogorovらの仕事に起源がある.)はKleeneの実現可能性(realizabikity)の概念を用いて正確なものにできる.

よくある誤解として,構成的数学は矛盾による証明を省いただけの数学であるというものがある.これは正しくない.次の典型例を考える.2は無理数である.これは2が有理数であるという仮定から始まる.そして初等的に議論を進め,完全に構成的な形で,矛盾に至るのである.このような議論は,完全に構成的な2の非有理性の証明といえる.実際,¬Pの構成的な解釈は,Pの仮定が矛盾を導くことである.この誤解は前述の証明を次のタイプの証明と混同することで生じる:

¬Pを仮定し,矛盾を導く.そして,Pが成り立つことを結論する.

これは非構成的である.

この視点を強化するために,次の形の証明を考える.
そのようなものは存在しないと仮定し,構成的な主張により矛盾に到達する.

このような証明には普通,そのようなものの存在を構成的に証明するアルゴリズム的な情報が含まれることはない.より形式的には,¬¬xP(x)の構成的証明から自動的にxP(x)を結論することはできない.

要約すると,¬pを証明するには,pを仮定して矛盾を導けばよい.pを証明するには,¬pを仮定して矛盾を導くだけでは,不十分である.

ここで,直観主義論理の実践に話を移そう.ある定理が性質P(x)が成り立つ対象xの存在を主張するとき,我々はどのようなものを求めるか.この定理の証明には,xの構成についてのアルゴリズムが骨格をなし,そしてxが性質P(x)をもつことが必要なだけ計算される.ここにいくつかの定理の例を挙げる.それぞれの定理に対し.その構成的証明のために必要な非形式的な記述がなされている.

A

すべての実数xについて,x=0x0である.

証明のために必要なこと(もの):実数xに対して適用されるアルゴリズムであって,x=0x0を決定するもの.ただしこの決定に際しては,アルゴリズムはxを記述するデータのみならず,xが実数であるというデータも用いることもできる.

B

すべてのRの非空部分集合Sに対して,それが上に有界(bounded above)ならば,最小の上界(a least upper bound)を持つ.

証明のために必要なこと(もの):実集合Sと,その元s,そして上界に対して適用されるアルゴリズムであって,つぎのようなもの.
(i) 対象bを計算し,bが実数であることを示す.
(ii) xbがすべてのxSに対して成り立つことを示す.
(iii) 実数b<bに対して,xSであってx>bとなるものを計算する.

C

fが閉区間[0,1]上の連続実数値写像でf(0)f(1)<0ならば,xであって,0<x<1かつf(x)=0となるものが存在する.

証明のために必要なこと(もの):函数fと関数fの連続度,そしてf(0)f(1)の値に対して適用されるアルゴリズムで,つぎのようなもの.
(i) 対象xを計算し,x0から1の間の実数であることを示す.
(ii) f(x)=0を示す.

D

fが閉区間[0,1]上の連続実函数写像でf(0)f(1)<0ならば,任意のε>0に対してxであって0<x<1,|f(x)|<εとなるものが存在する.

証明のために必要なこと:函数ffの連続度,そしてf(0),f(1)の値,そして正数εに対して適用されるアルゴリズムで,つぎのようなもの.
(i) 対象xを計算し,x0から1の実数であることを示す.
(ii) |f(x)|<εを示す.

(A)が構成的な証明を持つことを疑う理由はすでにある.(underflowのこと.これがBrowerian反例であることは前述の通り.)

(B)の証明の要件が満たされる場合.すべての数学の主張Pに対して我々はBの証明を適用することで,次の集合Sの上限σの有理近似zを計算することができる.
S={0}{xRPx=1}.ここでエラー<1/4とすると,σ>0のときz>1/4かどうかを,σ<1のとき z<3/4かどうかを決定できる.最初のケースの場合,xSそしてx>0,ここからx=1であり,Pが従う.もしσ<1ならば,¬Pが従う.したがって,(B)は排中律を導く.

しかしながら,ビショップの実数の構成的理論では,コーシー列の収束率が事前に定義されているがゆえに,構成的な最小上界原理を証明できる:

Sを非空部分実集合とし,上に有界とする.Sが最小上界を持つことと,それがupper-order locatedであることは同値.upper-order locatedとは,すべての実数α,β,α<βに対して,βSの上界であるか,あるいはxSであってx>αとなるものが存在する.

加えて,次のような別の(区間演算に基づく)Rの構成的理論の展開についても言及する.(→Bridges & Vîță)

(C)(D)は古典的には同値であり,中間地の定理である.この文におけるfの連続度とは,順序付けされた正数の組ε,δの集合Ωであって,次の性質がなりたつものである.
(i) すべてのε>0に対してδ>0(ε,δ)Ωとなるものが存在する.
(ii) (ε,δ)Ωx,y[0,1],|xy|<δに対して,|f(x)f(y)|<ε

(C)には異なる本質的に非構成的な原理,lesser limited principle of omniscience(LLPO)が含まれる:

(LLPO)

2値列(a1,a2,)であって高々一つがan=1であり,その他が0であるようなものは,an=0がすべての偶数nに対して成り立つか,an=0がすべての奇数nに対して成り立つ.

(D)(C)の弱い形であり,これは構成的に証明され,区間を半分にする標準的な議論を使う:

fが閉区間[0,1]上の連続実数値写像で,f(0)f(1)<0とする.fが局所的に非零とする.つまりx[0,1]r>0に対して|xy|<rf(y)0となるyものが存在する.このとき,0<x<1f(x)=0

中間地の定理の状況は構成的解析学における多くの典型的ものであり,我々は一つの古典的な定理に対していくつかの構成的バージョンを持っており,それらのいくつかが等価であることがわかる.

LPOやLLPOほど明確ではないomniscience原理がもう一つあり,それはマルコフ原理(MP)である.

(MP)

2値列(an)に対し,もしすべての項が0であることに矛盾するなら,ある項は1である.

この原理はいくつかの古典的な命題と同値である.例えば次のように:
(i) 実数xに対してx=0が矛盾するなら,x0
(ii) 実数xに対してx=0が矛盾するなら,yRであってxy=1となるものが存在する.
(iii) f:[0,1]R単射連続函数は,もしxyならf(x)f(y)である.

マルコフの原理は,非有界探索を表現している:

もしすべてのanが0であることが矛盾を導くならば,a1,a2,とテストしていくことで,かならず1の項が見つかることが保証される.しかしながら,この保証は宇宙の終わりまでに見つかるという保証には及びません.構成的数学の実践者のほとんどは,完全な不信ではないにしろ,少なくとも疑いの目でマルコフ原理をとらえている.この見解は,MPが構成的に導出可能でないことを示すKripkeモデルの存在により強化されている.(→Bridges & Richman)

【1】の終わりに

次回は【2】です.
参考文献
https://plato.stanford.edu/entries/mathematics-constructive/

投稿日:202373
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

I'm a second-year student at Shimokitazawa High School and play bass in the Kessoku Band. The articles I create are a team effort with Nijika Ijichi.

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中