論理学 [続き]

こちらが続きの方。で、 Shoenfield を読み始めたんですが、そもそも、この本って、大学の友達(あの古本おたくな友人たち)に古本屋で探してもらったんだが、うしろに「国井利泰」とか書いてある。あの国井先生のかよ〜



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



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



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



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



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



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



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



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