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