数学基礎論講義をこっそり読む(その8)

まず p.77 定理5.6(および定理5.8)に関してです。

『定理5.6
 1)Qにおいて表現可能な全域関数や関係は、すべて再帰的である。
 2)任意の再帰的全域関数、任意の再帰的関係は、Q上の適当な\Sigma_1論理式、ならびに適当な\Pi_1論理式でQにおいて表現される。』


おおっという感じですが、テキストでは証明がアウトラインだけになっているので、補足してみます。1)でいうところの全域関数と関係はメタレベルの話なのでそこでは使える道具に特に制限はありません。そこでQの公理系をゲーデルコーディングして算術化することで、


Prov_Q(x,y)yQにおける論理式のゲーデル数で、xはその論理式のQでの証明のゲーデル数である


なるような原始再帰的関係Prov_Q(x,y)が存在します。論理式や証明のゲーデル数化を記号\lceil A \rceilで表すとします。


さて、Qにおいて表現可能な関係をR(\vec{n})とし、それを表現する論理式を\varphi(\vec{x})とします。再帰的関係K(\vec{n})を次のように定義します。


K(\vec{n})\equiv Prov_Q( \mu x (Prov_Q(x,\lceil \varphi(\vec{\bar{n}}) \rceil)\vee Prov_Q(x,\lceil \neg\varphi(\vec{\bar{n}}) \rceil)),\quad \lceil \varphi(\vec{\bar{n}}) \rceil)


ややこしい形ですが、\mu演算で \varphi(\vec{\bar{n}})\neg\varphi(\vec{\bar{n}})の証明のどちらかになっているものを探索し、外側のProv_Qで見つけた証明がどっちの証明なのかを判定しています。R(\vec{n})が表現可能であることから、\mu演算の探索は必ず停止するのでK(\vec{n})は全域で定義された再帰的関係になり、かつ R(\vec{n})と等しくなります。つまり、R(\vec{n})再帰的関係としての表示が得られたことになります。
(蛇足ながら、2)があるので Prov_Q(x,y)自身がQで表現可能となってます。ここがおおっというところです。)


2)の証明中で省略されているところをいくつか補足します。
関数合成での証明に関して、例として\Sigma_1の一変数の場合を示します。\Pi_1の証明も同じようにできます。

m=h(g(n))のとき Q\vdash \exists y[\psi^\Sigma(\bar{n},y)\wedge \chi^\Sigma(y,\bar{m}) ] の証明:


k=g(n)とする。帰納法の仮定から、Q\vdash\psi^\Sigma(\bar{n},\bar{k})Q\vdash\chi^\Sigma(\bar{k},\bar{m})が成立している。
よって、Q\vdash \psi^\Sigma(\bar{n},\bar{k})\wedge \chi^\Sigma(\bar{k},\bar{m}) なので、\bar{k}のところを特称化すればよい。□


m\ne h(g(n))のとき Q\vdash \neg \exists y[\psi^\Sigma(\bar{n},y)\wedge \chi^\Sigma(y,\bar{m}) ] の証明:


k=g(n)とする。帰納法の仮定から、Q\vdash \neg(y=\bar{k})\rightarrow \neg\psi^\Sigma(\bar{n},y)Q\vdash\neg\chi^\Sigma(\bar{k},\bar{m})が成立している。



上の証明の結論の式でyを全称化して、\negを前に移動すればよい。□

次に\mu演算に関する証明ですが、テキストには誤植があります。たいしたものではないですが、\psi^\Sigma(x,y,0)等は\psi^\Sigma(x,y,\bar 1)でないと意味が通じません。本によっては特性関数で0と1が入れ替わった定義もあるのでそれと間違えたかと(担当筆者違うし。しかしよく見るとp.78の上から2行目は正しくなっている…)。[tex:\varphi(x,y)\equiv \psi^\Sigma(x,y,\bar 1)\wedge\forall z

Q\vdash \forall y(y=\bar{\mu k g(n,k)} \rightarrow \varphi(\bar{n},y)) の証明:


m=\mu k g(n,k)とする。帰納法の仮定より、Q\vdash \psi^\Sigma(\bar{n},\bar{m},\bar 1)かつ、[tex:k

Q\vdash \forall y(\neg(y=\bar{\mu k g(n,k)}) \rightarrow \neg\varphi(\bar{n},y)) の証明:


[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にしたらなぜ成立しないのか?)がすぐにわからなかったのですが、原始再帰法を\mu演算に置き換える定理4.31が定理5.9の原始再帰的関数の族に対しては使えません。そこで定理4.31のメタ証明をそっくりPA内部で再現することが必要になりますが、その際、Qでは力不足であるということだと思います。9.1節を待て!という感じでしょうか。

あと一点だけ気付いたことは、定理5.8の微妙な言い回しで、論理式が\Delta_1から取れるとは言っていません。これは一般的にQ\vdash \psi^\Sigma(x,y)\leftrightarrow \psi^\Pi(x,y)とならないためで、その差が生じるのはP.78の一番下の2つの論理式が同値にならないところからです。Q\vdash \forall x \exists ! y \psi^\Sigma(x,y)が成立しているとその同値が証明できるので、これが成立しないような再帰的全域関数が存在すると予想されます。
その例を示します。f(x)=equal(plus(0,x),x)とします。これは要するに1項関係 0+x=xですが、正直に翻訳すると

[tex:\varphi(x,y)\equiv *1\vee(\neg(0+x=x)\wedge(y=0))]

となります。以前のテキストPartAの前書きの問1と同じ論法で、Q\vdash \exists y \varphi(x,y)ですが、\exists! y \varphi(x,y)は証明できません(∵0+x=xQでは否定も肯定も証明できないため)。このとき\chi(x,y)\equiv (x=y) として、もし Q\vdash\exists y ( \varphi(x,y)\wedge (y=z)) \rightarrow \forall y ( \varphi(x,y)\rightarrow (y=z))が成立していると \vdash\varphi(x,z)\rightarrow \exists y ( \varphi(x,y)\wedge (y=z))なので Q\vdash\varphi(x,z)\rightarrow (\varphi(x,y)\rightarrow y=z) が出て、結局 \exists! y \varphi(x,y)が証明できて矛盾です。

*1:0+x=x)\wedge(y=\bar{1}