河野真治 @ 琉球大学情報工学です。

数学シリーズの続きです。結局、fj.comp.logic とか、fj.sci.logic
ってのは作らなかったのか。

僕は、自称、論理学者なわけなんですが、当時東工大にいた、吉田
夏彦先生に教えてもらったのは、論理学ではなくて哲学です。科学
哲学だね。前原昭二先生とかには、ゲンツェンの証明図式を授業で
習いました。僕が酒のみ二なのは、この酒のみな二人の影響が大き
いのは間違いない。

でも、学部の頃は、そんなんだったので、「数理論理学、記号論理
学、数学基礎論あたりは、まっとうな科学者なら、手を付けてはい
けないところだ」ってな印象が強かった。あの哲学の研究室は、そ
れで道を踏み外した人の溜り場みたいな場所だったから。

なんだが、大学院に行ったら、廻りがやっているのは Logic Programming
で、定理証明だとか、Resolution とか、エルブランモデルがとか
なんとか... Temporal Logic とか。おいおぃ。今まで避けてたと
ころばっちりかよ。しょうがないなぁ... まぁ、Prolog は流行だ
し。とか言いながら、実はやってみたかった分野だったし。

高校生の頃に、日本評論社の「数学の基礎」って本があってさ、こ
れが今から考えると、やっぱり外れの本で... 要するに 記号論理
学から ZF 集合論を勉強する本なんだけど、さぱり、わかりません
でした。「え、なんで、a ならば b で、a が成立しないと、「aな
らばb 」は真なんだよ」ってあたりで、けっつまずいてました。ま
ぁ、そのあたりは、前原先生の「記号論理入門」(あれも、日本評
論社だな...) とか授業とかで乗り越えたんだけど。

それ自体は簡単で「if 文の条件が成立しなければ、その式は実行
しなくて良い」あるいは、「Don't move or I will kill you = If
you move I will kill you 」ってことなんだけどさ。

で、大学院で使った教科書がMathematical Logic , Joseph R. Shoenfield 
　http://tinyurl.com/g986w
こいつ。これが難しい。今から考えると、なんで、前原先生の定番
の教科書(数学基礎論入門)を使わなかったのかが謎なんだが... 

で、 Shoenfield を読み始めたんですが、そもそも、この本って、
大学院の先輩に譲ってもらったんだが、うしろに「国井利泰」とか
書いてある。あの国井先生のかよ〜

最初に読む本じゃないんだよね。英語で読み始めたし。「モデルっ
て何?」みたいな感じ。それでも、がんがん読んで行く。Conservative
Extension ってなんだよみたいな。ゲーデルの述語論理の完全性っ
てのを、記号的なモデルを実際に構築することで証明していくわけ
なんですが、まぁ、難しいです。言葉は追えるんだけど、直観的に
わからない。不完全定理の証明もゲーデル番号を使った古典的なも
のだったし。

でも、その後で、Lloyd の Foundations of Logic Programming (
古い、もう売ってないのか... http://tinyurl.com/q7vlz ) を読
んだら、それは良くわかりました。

論理ってのが、文字列としての論理式と、その値に分かれるっての
が、理解できれば良かったわけ。その値の集合がモデルと呼ばれる
わけさ。で、そのモデルを、コンピュータ上の実際のデータ構造、
つまり、記号だけで構成されたものを使って作れるってのが、完全
性定理であり、Resolution であり、エルブランモデルだった。

で、モデルは論理式の値(へのマッピング)だから、それがわかれば、
証明とか検証とかも出来るってな話。そのマッピングを作るのがタ
ブロー法とか呼ばれるものなんだが...  残念ながら、そのアルゴ
リズムは、「いつかは終る」ならいいんだけど「正しければ終る」
みたいなものだった。

なので、正しさが人間的な視点から知り得ない整数論とかのモデル
は作れない。ってのが、ゲーデルの不完全性定理。プログラミング
の言葉で言うと、でたらめに試しているだけじゃぁ、正しいプログ
ラムには到達できないんだよってなこと。正しいプログラムはない
かも知れないんだからさ。あるんだったら、到達できるんだろうけ
ど。相手は無限なんだから、当り前。そういうことでした。

このあたりは、コーエンの連続体仮説の本が面白かった。こっちは
大学生の頃に読んだはずだが、「河野君、コーエンのForcingは、
もう古くて、Filter を使う方法が簡単なんだよ。Filter の定義は....
」ってな話を、その吉田研で食らって、実はわかりませんでした。
そのあたりから、話は、カテゴリー理論(圏理論)に突入するわけな
んだけど、残念ながら、「あ、な〜んだ、そんなことか」って言う
レベルには来てません。その時に教科書を聞いておけば良かったん
だが... 

カテゴリー論に興味が持てない理由の一つは、どうも有限な部分に
話が閉じないのでコンピュータに載らない話だからなんだろうな...
こういう有限な記号のモデルに自分自身を限定するのは、コーエン
では、V = L とかいうんだけど、かなり、V = L な奴です。人間っ
てのは、そういうもの。

そういえば、Forcing を使って、P=NP を解くという竹内先生の話
は進んだのだろうか? 

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科