コンピュータは数学者になれるのか？ 数学基礎論から証明とプログラムの理論へ

照井一成(著者)

• 販売会社／発売会社: 青土社
• 発売年月日: 2015/02/01
• JAN: 9784791768516

商品レビュー

2016/01/11

この分野、やっぱりおもしろい！
証明を端折ったストーリー展開と数学的厳密さのバランスが絶妙。学生の頃に感じたワクワク感を思い出しながら読めた。

2015/11/03

やや本格的な数学基礎論の本である。
手に取って少し読んでみるとわかるが、大学の教養程度の数学的知識があると読みやすい。

小学校で算数、中学生から数学という学問を学ぶ。
算数の授業では四則演算という「数」の基礎を勉強する。小学生足し算を勉強すると自然数がわかる。
次に引き算をすると、ある数に同じ数を引くと何もないという「０」を学ぶ。ある数にある数よりも大きい数をひくと負の数が出てくる。
掛け算は足し算の延長であることがわかるが、割り算となるとそうはいかない。
自然数や負の数、０でない数を導入する必要がある。有理数である。

そして二次方程式を勉強すると、２乗して２になる数という未知の数が出てくる。これを無理数と呼ぶ。
先の有理数と併せてこの体系を実数と呼ぶ。
これで打ち止めかと思ったら、二乗して負になる数を考える。虚数である。
実数と併せて、この体系を複素数と呼ぶ。

大学ではさらに複雑な数をいくつも学ぶことになるが、そもそもこれらの数はどのように導入してきたか？

ある定義を与えて、それを演繹的に演算することで定理を証明していく。
たとえば、1+2+3＋・・・・+n=n(n+1)/2となることを証明しよう。
高校までの知識で解くことができるだろうか？
高校までの知識とは、というところで議論がわかれるかもしれれないが、大半の人は「数学的帰納法」を使えばよい。と答えるかもしれない。
たしかに、数学的帰納法によって
１）n=1のとき成り立つ
２）n=kのとき成り立つと仮定し、n=k+1を計算すると、
1+2+・・+k+(k+1)
=k(k+1)/2+(k+1)=(k+1)(k+2)/2
となり、確かにn=k+1のときも命題は成り立つので、すべての自然数に対して、命題は成立する。　（証明終）

なるほど、確かに上記の議論は正しいし、期末テストで上記を解答すればマルをもられるだろう。
しかし、数学的帰納法は数学的に正しいことを前提としていえるが、これはどこから来たのか？
教科書ではドミノ倒しのイラストがのっており、なんとなくイメージはつくが、全然証明になっていない。

このように証明とは何か、数とは何かという数学の基礎の基礎は実は学ぶ機会が少ない。
これは特に意識しなくとも、数学が確固たる基盤の上で展開されているため、いちいち気にしなくとも問題ないという、過去の数学者の血と汗（と涙）の結晶であるためである。

本書はその基礎そのものについてスポットをあてる。
まず気になるのは出発点はどこか。ということであろうか。
昔、子供のときに○○は何で出来ているの？ゲームをしたことはないだろうか？
これを繰り返していくと、それ以上還元できないところが出てくる。普通の人なら、何で出来ているかゲームは原子（または素粒子？）でゲーム終了ではないだろうか。しかし、あくなき好奇心を持つ子供は、じゃあ素粒子は何で出来ているの？と聞いてくるが、これについては苦笑いで沈黙するしかない。
だってこの先は誰も知らないのだから。。。

数学も同じである。遡っていくとこれ以上、証明できない命題が出てくる。これを公理と呼ぶ。
公理は、これ自体証明する必要がないため、勝手に考えていい。例えば、１＝２を公理として採用しても良い。が、あまり良い数学体系にならない。
ということで、あまりに勝手に公理を取ると体系がめちゃくちゃになるが、少なすぎると、そこから生まれる体系が芳醇にならない。
つまり、必要最低限で互いに独立な公理系が最高にHappyだ。

ある公理を数個持ってきて、それが互いに独立であることは（難しいけれど）判断することができる。
なぜならば、公理A,B,CをとってきてAとBからCが証明できれば、Cは公理系として選ぶ必要はない。この場合、公理A,Bで十分ということになる。
問題は、公理A,Bの二つで十分かということである。
これは大変難しく、歴史的な問題である。

20世紀初頭に数学者の間でこれについて議論がおこった。
Hilbertは、互いに矛盾がなく、独立な公理系を選ぶことができるという考えのもと、Hilbert問題という問題を提起した。
が、これはGedelによって否定的に解決された。
つまり、どんな公理系を選ぼうとしても、その公理系で決定不可能な命題が存在するというのだ。
（決定不可能とは、その命題が真か偽か証明できないということ）

これは数学の限界を与える定理と呼んでもいいのかもしれない。

しかし、悲観してもしょうがないので、どの程度無矛盾なのか、どうやれば無矛盾をいい方向に持っていくことができるかという前向きな議論が重要である。
この点、本書に詳しく議論されている点である。

2015/09/26

150926 中央図書館
論理規則を確認して証明図を一つ一つ確認するのは普通の読者には難しい。しかし数学の難題に対して自動証明の手法が挑戦している状況は、この本を手に取らなければ想像もしなかったところ。終章に引かれているケプラー予想の証明確認の経緯が象徴的。