北田 発見への道 7章

7章 ゲーデルナンバリング

項・式・証明列が与えられた時、それらを一意に自然数にエンコードすることが可能である。このエンコードの規則をゲーデルナンバリングと呼ぶ（その実装には任意性がある）。その自然数を体系内の自然数と同一視し、変数x にその自然数を代入できる。この操作はSのメタの理論のモデルを対象とするモデルに作成することに対応し、意味論的操作である。

ゲーデル述語 R(a,b) として、「aは式Aのゲーデル数であり、bはAの証明のゲーデル数である」を定義すると、可証性述語すなわち、「式Aの証明が存在する」というメタな述語は、「 ∃b R(a,b)」と表現できる。R(a,b) は数値的に表現可能であるので（2個の自由変数をとるある式 r(a,b) で表現できるので）、可証性述語は 「∃b r(a,b) 」とかけ、「Aは証明できない」という述語は、「∀b￢r(a,b)」と書ける。

対角定理に、この h(a) = ∀b ￢r(a,b) を代入すると、「G ⇔ ∀b ￢r(g,b) 　すなわち、いかなる証明列もGの証明でないというGが存在する」と意味する言明が得られる。同様に、￢G は「ある証明列はGの証明である」に対応するため、「￢G⇔ ∃b r(g,b)すなわち、 ある証明列は G の証明である。」こうして、証明も反証もできないゲーデル式Gが構成できると考えられる。

実際、このような文はロッサー文として、具体的に書き下すことができる。ロッサー文およびその否定は、Sにおいて証明可能でない。

議論はまぁ明快。対角化定理の証明が乗っていない。ロッサー文は、拡張されたゲーデルの不完全性定理といわれているらしいが、どこをどう拡張したのかは書かれていないのが不満。個人的には、関係の数値的に表現可能なことは自明で、任意の関係について成立しそうに思うのだが、なにか勘違いしていそうな予感。