数学基礎論講義をこっそり読む(その8)
まず p.77 定理5.6(および定理5.8)に関してです。
『定理5.6
1)において表現可能な全域関数や関係は、すべて再帰的である。
2)任意の再帰的全域関数、任意の再帰的関係は、上の適当な論理式、ならびに適当な論理式でにおいて表現される。』
おおっという感じですが、テキストでは証明がアウトラインだけになっているので、補足してみます。1)でいうところの全域関数と関係はメタレベルの話なのでそこでは使える道具に特に制限はありません。そこでの公理系をゲーデルコーディングして算術化することで、
⇔ はにおける論理式のゲーデル数で、はその論理式のでの証明のゲーデル数である
なるような原始再帰的関係が存在します。論理式や証明のゲーデル数化を記号で表すとします。
さて、において表現可能な関係をとし、それを表現する論理式をとします。再帰的関係を次のように定義します。
ややこしい形ですが、演算で かの証明のどちらかになっているものを探索し、外側ので見つけた証明がどっちの証明なのかを判定しています。が表現可能であることから、演算の探索は必ず停止するのでは全域で定義された再帰的関係になり、かつ と等しくなります。つまり、の再帰的関係としての表示が得られたことになります。
(蛇足ながら、2)があるので 自身がで表現可能となってます。ここがおおっというところです。)
2)の証明中で省略されているところをいくつか補足します。
関数合成での証明に関して、例としての一変数の場合を示します。の証明も同じようにできます。
のとき の証明:
とする。帰納法の仮定から、とが成立している。
よって、なので、のところを特称化すればよい。□
のとき の証明:
とする。帰納法の仮定から、とが成立している。
上の証明の結論の式でを全称化して、を前に移動すればよい。□
次に演算に関する証明ですが、テキストには誤植があります。たいしたものではないですが、等はでないと意味が通じません。本によっては特性関数で0と1が入れ替わった定義もあるのでそれと間違えたかと(担当筆者違うし。しかしよく見るとp.78の上から2行目は正しくなっている…)。[tex:\varphi(x,y)\equiv \psi^\Sigma(x,y,\bar 1)\wedge\forall z
の証明:
の証明:
[tex:\neg\varphi(\bar{n},y))\equiv \neg\psi^\Sigma(\bar{n},y,\bar 1)\vee\exists z(z
次に p.79 定理5.9に関してです。
定理5.8とどこが違うのか(PAをQにしたらなぜ成立しないのか?)がすぐにわからなかったのですが、原始再帰法を演算に置き換える定理4.31が定理5.9の原始再帰的関数の族に対しては使えません。そこで定理4.31のメタ証明をそっくりPA内部で再現することが必要になりますが、その際、Qでは力不足であるということだと思います。9.1節を待て!という感じでしょうか。
あと一点だけ気付いたことは、定理5.8の微妙な言い回しで、論理式がから取れるとは言っていません。これは一般的にとならないためで、その差が生じるのはP.78の一番下の2つの論理式が同値にならないところからです。が成立しているとその同値が証明できるので、これが成立しないような再帰的全域関数が存在すると予想されます。
その例を示します。とします。これは要するに1項関係 ですが、正直に翻訳すると
[tex:\varphi(x,y)\equiv *1\vee(\neg(0+x=x)\wedge(y=0))]
となります。以前のテキストPartAの前書きの問1と同じ論法で、ですが、は証明できません(∵がでは否定も肯定も証明できないため)。このときとして、もし が成立していると なので が出て、結局 が証明できて矛盾です。