読者です 読者をやめる 読者になる 読者になる

Redundanz

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

0111

logic

 いつもより解像度の高い一日でした。世界が爽やかに見える。上手く眠れたからかな。朝起きて、大学へ行って、講義を受けてという流れが、清々しいものに思われて、上手く言えないけれど、丁寧に生きられた気がしました。こういう日がもっと増えると良い。

 大学終わって、その後バイト。今日はここでも割と頭が冴えていて、世界救えたかなと思います。何人ものスタッフを倒した問題を解決すること、敵討ちっぽくて楽しい。
 「a,b,cが3より大きな素数であり、2a+5b=cを満たす時、a+b+cは自然数Pの倍数となる。この時Pの最大値を求めよ。」とか面白かったです。そんなに難しいわけではないけれど、意識的な思考と着実な推論の積み重ねで解答に到達するの、考えてるなーって実感があって気持ちが良い。ちなみに答えは9なのだけど、9以上ではないことの示すのにもう少し上手いやり方がありそうで、もう少し考えてみようかな。

 帰りの電車の中でゲーデルと20世紀の論理学のペアノ算術の項目を読み直していたら、これまでよく分かっていなかったことがストンと腑に落ちる感覚があって、ほんとうに良い気分でした。

 自然数の標準モデルというのがあって、それは僕らが一般的に正しいことを直感的に知っている数論の決まりとその解釈なのですが、それを、整備された公理系が表現できること、写し取れることを示す必要があります。
 まずペアノの公理を構成する要素として、定数0、関数記号S,+,・、等号=、不等号<、論理記号¬,∨,∧,→,⇔,∃,∀があります。
 例えば後者関数SについてS(0)は、自然数上で解釈するところの1(0の後)なのですが、これはそう解釈が可能だというだけで、本来的にはS(0)以外の何ものでもないのです。それが形式的な体系であることの所以であり、力であるということを納得するのに、割と時間がかかりました。
 それから、これらの記号のみでは計算ができないので、公理を加えます。
 まず後者関数について
 ∀x¬(S(x)=0)
 ∀x∀y*1→(x=y))
 これが何を言っているかというと、0にSを付けたり外したりして到達できるもの全体は、0を始点として合流や枝分かれのない一本の筋になっているということです。これにより、自然数との一対一対応を考えることが出来るようになります。
 足し算に関する公理
 ∀x(x+0=x)
 ∀x∀y(x+S(y)=S(x+y))
 掛け算に関する公理
 ∀x(x・0=0)
 ∀x∀y(x・S(y)=(x・y)+x)
 上記の公理だけで、足し算、掛け算は全て再帰的に実行できます。0の何番目か後という風に形式的に定義された数同士の積和が、再帰的に0の何番目か後であるというふうに求まるのです。
 例えば、3+2は、ペアノ算術上で表現すれば
   S(S(S(0)))+S(S(0))=S(S(S(0))+S(S(0)))=S(S(S(0)+S(S(0))))=S(S(S(0+S(S(0)))))=S(S(S(S(S(0)))))

 と書けるわけですが、これは単純に上の公理のみ適用しただけです。これらの決まりごとだけで計算が実行できること、凄いなと思います。
 それから、不等号に関する公理と、帰納法の公理(これが無限にあるというの、なんか楽しい)があるのですが、書くのが面倒になってきたので省略します。

 このように、ペアノ算術がいろいろな計算を実行できることが分かるわけですけども、それはまだ証明されたわけではないので、メタの立場からそれは示してやる必要があります。つまり、自然数論上の論理式が、ペアノ算術で書けることを示してやるのです。ただ、ペアノ算術で書ける種類の論理式というのは制限があるので、ここでまず��1,Π1,Δ1という論理式の種類を定めてやり、その内の��1論理式に関しては、自然数論上で証明可能な��1論理式がペアノ算術上で証明できることを証明します。これが、��1完全性定理です。
 僕はこれを証明する過程を上手く理解できていなかったのですが、先のペアノ算術上での足し算掛け算の正当性が、帰納的に示されるその道筋と同様のやり方を適用すれば良いことがわかり、それで何もかもしっくりきたのです。上手く書けないし、これを読んだ人が何かを得られるとも思えないのですが、自然数論上の数mをPAにおけるm(上にバーがついてるアレ)に対応させる再帰的なやり方、の必要性を僕ははじめて理解できたことになります。ひゃっほーう。

 ここで��1論理式の完全性を示した後、今度は、自然数上の関数や述語がPAで「表現可能」であることを示します。これがどういうことかというと、自然数論の一般的な解釈をした際に、その述語や関数を意味しているよう考えることの出来るPA上の論理式、というものを考えるのです。これは形式的なものであり、値を代入すればある値を返すというそれだけなのですが、ともあれ、頑張れば自然数上の述語や関数として解釈できる、というようなものです。この「表現可能」を定義した後に、��1論理式が表現可能であることを示すわけですが、それはすなわち次のように書かれます。
 PAにおいて表現可能な関数や述語は、全て計算可能である。
 任意の計算可能関数、計算可能述語は、適当な��1論理式、ならびに適当なΠ1論理式でPAにおいて表現される。
 このことの証明は、なんというかあまりに壮大で、無限の論理式の列を生成すれば、その内何か一つは、PAにおいて自然数論上の述語を表現したものである、というようなヤバ気な話なのですが、それでも形式的には何の問題もないわけで、凄いです。楽しい楽しい。
 そうして、計算可能関数の表現可能性定理というところに向かってゆくわけなのですが、何を書いているのかよく分からなくなってきたのでこの辺でやめます。一晩寝たらもう少し頭が整理されているはず。
 この日記始まって以来の意味不明な記述になったけども、そのくらい僕は興奮していたわけで、この感覚を、後に残して、好きに思い起こせればいいな、とか。そうしたら僕の精神生活ももう少し素敵になるはずなのだ。考えるのは楽しい。いつだってそれを念頭に置いて置きたいなと思います。

 部屋を掃除せねばなりません。明日は生活を素敵にするアイテムを幾つか手に入れにゆこう。

*1:S(x)=S(y