Redundanz

僕の言葉は、人と話をするためにあるんじゃない。

不完全性定理とか。

講義だけでは理解できなさそうなのと、万が一朝起きれなくて欠席した場合、講義についてゆけなくなることを考えて、ゲーデルと20世紀の論理学③読み始めました。岡本教官の講義と、だいたい同じように進んでゆくので、正直こちらで勉強しても良い気がします。まあ、あの方のdisり芸眺めるのは面白いし、授業には出よう。(また敵を作るようなことを)

とりあえず、今日は第一章を。計算可能関数とそれと同値な概念として再帰的関数が定義されました。この定義する、というの、未だに慣れません。高校まではだいたい自明だけども、ちょっと細部が甘いからしっかり補強する、程度の営みだと甘く考えていたのですけど、読み進めていると、定義が4つデンと書いてあってそれで終わりという風な書き方が殆どで、ええ、つまりどういうことなの説明してよ、となります。(だからそういうことではないのだ)まあ今までの順序がおかしかった、というのは言いすぎかもだけど、そういう領域に入ってきたのだなあと、ちょっと身構えます。でも具体的に考えながらだとまだわかるので、セーフ。(メモ:定義(3)(原始再帰のとこ)の式はまだ良くわかってない)
ところで、概念自体は把握できるのですけど、それがどうして導入されたものなのかはまだわかりません。原始再帰的関数(再帰的関数から最小化を除いたものらしい)がどうしてここで出てくるのか、とか。Recuという自然数上の関数のクラスを使えば、原始再帰は消去できるらしいので、これが形式体系を自然数でコードすることに関わってくるのかな。まあいつかわかる日が来るでしょう。
そういえば再帰的関数が計算可能性の概念と同値であることは、どうやって証明されるのだろうか。(本では省かれていた)つまり再帰的関数の定義により与えられる再帰的関数が、計算可能関数を過不足なく網羅していれば良い気がするのだけど、それはどういうことなのかな。ゼロ関数、後者関数、射影関数が計算可能関数であることが言えればいいのだろうか。あらゆる再帰的関数がそれらの合成で出来ていることは言えない、のか。ああでも、この4つがそうだと言っているのだから、言えるのかな、とか。定義する、というの、凄まじい仕事だと思います。本当に。
この形式体型を自然数でコード化するというお話、ふと考えると、二進法でもいいわけで、ああチューリングマシンの概念とこの辺で繋がってはいるのねと、ほっこりしました。(もちろんチューリングマシンも2進数でなくたって良い)実際先のページをちらと読んでみると、その辺言及されていて、ちょっと嬉しかったです。

長々と書いてはみたけれど、あんまり理解できている気はしません。(見る人が見たら怒り出すかもわからん)けれども、一度自分なりに思ったことを書きだしてみて、わからんことがすごくわかってないことくらいは認識できたので、少しずつこの辺にまとめてゆこうと思います。
知りたいことを知るために知らなきゃならないこと、ぞっとするほど多いです。僕に、切り崩せるだろうか。こわわ。

あと、ちょいちょい出てくるのだけどノイマン氏やばい。あんな風になりたかった。