この記事の問いと内容
この記事では、「コンピュータは数学者になれるのか 数学基礎論から証明とプログラムの理論へ」という本を紹介したい。数学、論理学、人工知能、プログラムをまたぐ、とんでもなくエキサイティングな本になっている。
・数学するという行為は、記号、形式に還元可能なのか?
・数学者の数学という行為を、どうやってコンピュータで再現させるのか?
・再現できるとするなら、人工知能は人間知性を超えたと言っていいのか?
・数学の本質、プログラムの本質、またそれらの間の関係の本質とはなにか?
こんな問いに興味がある人には、ぴったりな本だと思う。これらテーマのもと、数学基礎論という抽象的な議論を追うことになる。そこには、あの不完全性定理も、もちろん登場する。
数学するとはなにか。それは、「証明とはなにか?」を考えることへ向かう。
そして、人工知能の中身であるプログラムと数学、証明の関係を丁寧にひも解いていく。人工知能を数学から理解したい人にも欠かせない一冊になるはずだ。
この記事ではざっくりとした紹介になってしまう。前提知識がない人にはかなり読みづらいと思う。雰囲気をつかんでみてほしい。
- この記事の問いと内容
- コンピュータは数学者になれるか 照井一成
- 数学者を作りたい! 数学の形式化
- 計算の停止と無矛盾性
- NPという壁
- ラムダ計算
- 真理条件と検証条件
- 証明の意味って?
- 今後の展望
- 関連記事
コンピュータは数学者になれるか 照井一成
「計算」や「論理」がいかにして現実を変革するのか? ヒルベルト、ゲーデル、チューリング、ゲンツェンら天才たちの挑戦は、いまコンピュータ科学を経由して、世界に大転換をもたらしつつある。「不完全性定理」「P対NP問題」などの論争の歴史を最新アップデートし、「人工知能」の未来にまで架橋する数理論理学の決定版!
個人的に何度も読み返している超おすすめ本。
この記事では、主要な論点、流れをまとめてみたい。
数学者を作りたい! 数学の形式化
数学すること、推論することを形式化する。「意味」をすて、形式的な記号で表現する。
数学を形式的な記号で表すことにより、「数学すること」を数学できるようになる。それは、数理論理学や数学基礎論として研究されてきた。そこには、次のような目標があった。
「自分に似せて数学者を作ろう、そして彼・彼女が無矛盾なことを証明しよう」
完全かつ無矛盾であるという性質が数学をやるうえで重要になる。だから、それを証明したい。
しかし、その形式的体系にはある限界が見つかる。あのゲーデルの不完全性定理だ。
形式的理論には、数学を完全に写し出す力がない
自己完結的な確実性は、不可能になった。
不完全性定理についてさらに知りたい人は、次の記事は進んでみてほしい。
本書のおもしろいところは、不完全性定理のような「できない」に注目するだけではなく、「どこまでできるのか」まで紹介してくれるところだ。それが、ゲンツェンの存在である。そして、証明とプログラミングの関係へと話は進んでいく。
計算の停止と無矛盾性
「計算の停止」という概念は、証明図の書き換え、つまり、証明することと結びついていく。
その帰結が、ゲンツェンの無矛盾性証明だ。
整列集合
超限順序数
ペアノ算術の無矛盾性証明
NPという壁
ラムダ計算
・カリーハワード対応
カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry-Howard correspondence)とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワードにより最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種と関係している。
真理条件と検証条件
・直感主義論理
証明の意味って?
今後の展望
「数学基礎論に端を発する証明とプログラムの理論は、いわばゲーデルを横軸とし、ゲンツェンを縦軸としつつ、対角線方向に発展してきたといってよいのではないかと思う。」
関連記事
論理学、人工知能についての記事を紹介する。