この記事の問いと内容
「コンピュータは数学者になれるのか 数学基礎論から証明とプログラムの理論へ」という本を紹介したい。数学、論理学、人工知能、プログラムをまたぐ、とんでもなくエキサイティングな本になっている。
・数学者の数学という行為を、どうやってコンピュータで再現させるのか？？
・再現できるとするなら、人工知能は人間知性を超えたと言っていいのか？
・数学とプログラムの関係の本質とはなんだろう？
こんな問いに興味がある人には、ぴったりな本だと思う。これらテーマのもと、数学基礎論という抽象的で深い流れを追うことになる。そこには、あの不完全性定理も、もちろん登場する。
数学するとはなにか。それは、「証明とはなにか？」というテーマに行き着く。
そして、人工知能の中身であるプログラムと数学、証明の関係を丁寧にひも解いていく。人工知能を数学から理解したい人にも欠かせない一冊になるはずだ。興味がある人は、まずは目次に目をとおしてほしい。
数学者を作りたい！ 数学の形式化
数学すること、推論することを形式化する。「意味」をすて、形式的な記号で表現するのだ。
数学を形式的な記号で表すことにより、「数学すること」を数学できる。数理論理学や数学基礎論として、研究されてきた。そして、次のような目標があった。
「自分に似せて数学者を作ろう、そして彼女が無矛盾なことを証明しよう」
しかし、その形式的体系に、ある限界が見つかってしまった。あのゲーデルの不完全性定理だ。
形式的理論には、数学を完全に写し出す力がない
自己完結的な確実性は、不可能になった。
不完全性定理についてさらに知りたい人は、次の記事は進んでみてほしい。
interaction.hatenadiary.jp
本書のおもしろいところは、不完全性定理のような「できない」に注目するだけではなく、「どこまでできるのか」まで紹介してくれるところだ。それが、ゲンツェンの存在である。そして、証明とプログラミングの関係へと話は進んでいく。
整列集合
計算が止まるかどうかは、日常のソフトウェアの使用を考えてみても重要な問題。永遠に計算が止まらなかったら、ソフトウェアを信頼できない。
停止することをなんとか示したい。それなら、数学的に証明してやるのが一番確実。
停止性証明のために、「整列集合」が使える。たとえば、自然数は無限に小さくなることはない。自然数の集合は、整列集合になる。この整列性を利用して、計算が止まることを示すことができる。
超限順序数
数の拡大のために、「無限の向こう側」を認める！！！
順序数とは、ざっくりいうと、無限大よりも大きい数をどんどん構成していくことを認めて作り出した数。
そして、この順序数をもちいて、いくらでも大きな整列集合を作ることができる！
ここで、「順序同型」という性質がある。
２つの集合が、順序関係についてそっくりであることだ。そして、ある条件を満たす、整列集合と順序数の集合は、順序同型になる。さらに、順序数の集合そのものも、整列集合といえる。
何度も無限の向こう側へジャンプしたはずなのに、下方向へは有限になる！
「まるでお釈迦様の手の上の孫悟空のよう」という著者の比喩は、とても興味深い。
ペアノ算術の無矛盾性証明
カントールの順序数が武器になる。
順序数は整列しており無限下降列を持たない。証明図に順序数を割り当てる。証明図を書き換えていった時に、順序数が小さくなるなら、書き換えは停止する。
さらに、ある順序数に注目することで、PAという形式系の無矛盾性は有限の立場で証明できる。これが、ゲンツェンの無矛盾性証明だ。
しかし、その「ある順序数の整列性」を、PAは証明できない！
ゲーデルの第二不完全性定理は、「自分の無矛盾性を証明できない」と言っているにすぎない。ゲンツェンの証明は「自分の無矛盾性を証明させようとすると、具体的に何でつまずくのか」をあきらかにしてくれる。
ここに注目し、第二不完全性定理を無矛盾性証明とともに使うという方向性がみえてくる。
「形式系の無矛盾性」と「計算の停止」には共通点が多い！！
どちらも、書き換えが有限回で終わることを示すのが目標になる。
NPという壁
「しらみつぶしに探せば解ける問題は、常に素早く解けるか」これが、P対NP問題である。
しらみつぶしを克服する方法の一つが、うまい定理を見つけることだ。法則が見つかれば、ぐっと計算を効率化できる。つまり、「知性によりしらみつぶし的状況は克服できるか」が本質になる。
現状、P ＝NPは否定的である。ある問題に対しては、素早く解けるような定理は見つかるはずがない、と考えられている。
このNPの壁は、人工数学者における証明をどう見つけるかということに関わる。証明図を見つける理論的な解法の存在は否定されてしまう。
ラムダ計算
・ラムダ計算
・BHK解釈
・カリーハワード対応
カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry-Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。
カリー＝ハワード同型対応 - Wikipedia
ラムダ計算では、数学的対象をすべて関数だとする。
ラムダ計算でも、真偽、論理演算子、関数の合成、自然数、足し算などの基本演算を表現できる。さらに、再起的プログラミングまでできる。よって、ラムダ計算はチューリング機械と同等のパワーをもつ。
証明図の構成要素である論理式を、ラムダ項であらわせる。しかし、背理法の規則だけはラムダ項を割り当てることができない。
背理法を取り除いた論理システムを直観主義論理という。
こうして、証明図を与えられたら、順にラムダ項で解釈していける。BHK解釈という。ということは、「証明はプログラムである」というテーゼが出てくる！！！！
証明はプログラムと対応し、証明の書き換えはプログラムの実行と対応し、論理式は型とみなせる。→カリーハワード対応
ラムダ計算は、関数型言語のもと。
さらに、証明がプログラムであるならば、証明からプログラムを抽出することができる。証明図からプログラムを抽出する方法を、構成的プログラミングという。
人間が証明図を作成するのをサポートする目的をもつのが証明支援系だ。
論理主義、形式主義、直観主義の融合ともいえるパラダイムをベースにしているCoqなどがある。
カリーハワード同型対応については、次の記事でもまとめている。
真理条件と検証条件
・直感主義論理
よって、構成的証明ではこれらは使えない。「Aでなくない」から「A」を導くことはできない！！
古典論理では、「どんな文も真か偽である」という２値解釈をもとに、「どのような条件のもと文は真になれるか」という真理条件を考える。
一方、直感主義論理では、文の意味は、「何をもって文の検証とみなすか」という検証条件として与えられる。つまり、文の意味とは「構成」「手続き」という操作によって定義される。
ある古典論理を、直感主義論理へ翻訳することもできる！これは、非構成的な証明から構成的情報を取り出そうという動きもになる。
証明の意味って？
証明は、連続写像（切れ目のないグラフのイメージ）とみなせる。
計算可能であるならば、連続といえる。
「証明＝プログラム」には、圏論的な見方も応用できる。
そもそも、プログラミング言語は記号に過ぎない。だから、どう解釈すべきか厳密に定めたい。記号、プログラム、証明に意味を与えよ、となる。
自動定理証明システムは、証明から意味をはく奪する。
一方、定理証明支援系は、構成的な意味を使う。「活き活きした証明」と著者は強調している。
これらは、カラーハワード対応を土台とする「証明とプログラムの理論」の真髄といえる。
今後の展望
