[雑記]雑記2008年1月1日(火)

■ ゲーデルと年越し

• 『ゲーデル 不完全性定理 (岩波文庫)』

ゲーデル(著), 林晋(訳), 八杉満利子(訳)

岩波書店、2006

『不完全性定理―数学的体系のあゆみ』を読んでいたのだけど、歴史的解説ばかりで読むのがたるくなってきて、「計算させろ！ 証明させろ！」と本編「プリンキピア・マテマティカおよび関連した体系の形式的に決定不能な命題についてI」に突入してみた*1。思うんだが、こんなもの口で説明されても、手を動かさないと絶対わからんと思うんだよね。もしもわたしがゲーデルの解説書を書くんだったら公文式みたいなドリル形式のやつにするけどなあ。そういうのどっかで出てないかな。

というわけで読みはじめたのだが、もっと全然歯がたたないかと思ったのに意外に意味がわかる。と言ってもまだはじめのところなのですぐまた難所にぶつかるかもしれないけど。なるべく証明を追いかけたり、自分で解いたりしながら、ゆっくり進めます。

とりあえず最初の方は、ラッセルのタイプセオリーについて初等の知識があったのが大分助けになった。『哲学の歴史 11 20世紀 2 (11)』の戸田山和久氏の論文と、岩波新書の『ラッセルのパラドクス』を読んでいたのがよかった。

あとなんでプログラマーが変数の「型」って言うのかよくわかってなかったけど、これ読んでイメージがつかめた。「型」ってまさにタイプセオリーのタイプのことだったんだなあ。

http://ja.wikipedia.org/wiki/%E5%9E%8B%E7%90%86%E8%AB%96

細かい歴史的経緯はよくわからないが、紆余曲折を経て、ラッセルパラドックスのおかげで型付きの言語が生まれたと言えなくもないのか*2？

あとこれはみんな思うことかもしれないけど、読んでいるとどうしてもプログラムで書いてみたくなる。ゲーデルコード化する関数なんてまさに計算機むきではないかと思うんだけれど。そういえば、ゲーデルは証明をLispで書くべきだったと、無茶なことを言った人もいたそうです。

http://www.unfindable.net/~yabuki/article/why_lisp.html

ちなみにゲーデルコード化はどう書く?orgの問題にもなっている(正の整数だけだけど)。

http://ja.doukaku.org/100/

自分でも何か書いてみたいが、無限集合や全称量化を計算機でどう扱えばよいのかがいまいちわからないなあ。そう言えばRubyにSetクラスあったなと思って見てみたけど、これじゃ無限集合扱えないじゃないか。

http://www.ruby-lang.org/ja/man/?cmd=view;name=set

集合自身にメンバーへの参照を持たせず、メンバーかどうかを判定する関数だけを用意すれば無限集合を扱える気がするんだが、誰かそういうノウハウを公開してないかなあ。

あと以下は自分用のメモ。

• 『数学基礎論入門 (基礎数学シリーズ) (単行本) 』
• 『数学基礎論入門』

この本はよさそうだ。

あと↓この本ちょこちょこやってる。

• 『集合論入門 増補版 (単行本) 』

数学楽しい。

■ 去年のベストとか

書こうと思って放置している。

まだ選んでもいない。

こういうのって新年になってから発表したらまずいものだっけ。

■ 名所めぐり

新年からぐだぐだな感じでだべったりとらのあなに行ったりした。

どうでもいいが、「虎穴に入らずんば虎児を得ず」の対偶は「虎児を得たならば虎穴に入った(ある人が虎の子供を得たならば、その人は虎の穴に入った)」である。言いかえるとずいぶん印象が違う。

• *1: ダンコガーイも解説書なんて薦めないで、こっちを紹介すればいいのに
• *2: このあたりの哲学・論理学用語から計算機用語への転換の過程について細かく調べたらおもしろいだろうと思うのだが、その手の情報ってどこにも転がっていないので困る。具体的に言えば「変数のスコープ」とか「クラスとインタンス」なども哲学・論理学用語の流入だろうと思うんだが、いまいちどっからどう流れたのかがよくわからずにいる。