論理式の表現可能性
算術
自然数$ xに対して数項$ \bar{x} = \underbrace{S(S(\cdots S}_{x \text{ times}}(0) \cdots )
自然数の上の関数$ f(x_1\dots,x_n) = yが表現可能(representable)であるとは,
自然変数$ n+1個の自由変数$ x_1,\dots,x_n,yを含んだ論理式$ A_f \lbrack x_1,\dots,x_n,y \rbrackが次の条件を満たす
1. $ f(x_1,\dots,x_n)=yのとき,論理式$ A_f \lbrack \bar{x_1},\dots,\bar{x_n},\bar{y} \rbrackが証明可能.
2. $ \forall x_1 ,\dots, \forall x_n \forall y \forall y' \left( A_f\lbrack x_1,\dots,x_n,y \rbrack \land A_f\lbrack x_1,\dots,x_n,y' \rbrack \to y = y' \right) が証明可能
1. 定数$ 0
論理式$ A_0 \lbrack y\rbrackを$ y = 0
2. 後者関数$ \text{succ}(x) = x+1 論理式$ A_{\text{succ}}\lbrack x,y\rbrackを$ y = S(x)
3. 射影関数$ \text{proj}(x_1,\dots,x_n) = x_i(ただし$ 1 \leq i \leq n)
論理式$ A_{\text{proj}}\lbrack x_1,\dots,x_n,y\rbrackを$ y = x_i
4. 合成関数$ h(x_1 \dots x_n) = f(g_1(x_1,\dots,x_n),\dots,g_m(x_1,\dots,x_n))
論理式$ A_{\text{proj}}\lbrack x_1,\dots,x_n,y\rbrackを
$ \exists y_1,\dots,\exists y_m \left(A_{g_1} \lbrack x_1,\dots,x_n,y_1 \rbrack \land \cdots A_{g_m} \lbrack x_1,\dots,x_n,y_m \rbrack \land A_{f} \lbrack y_1,\dots,y_m \rbrack \right)
5. 原始再帰関数$ f,gについて
$ h(0,x_1,\dots,x_n) = f(x_1,\dots,x_n)
$ h(S(x),x_1,\dots,x_n) = g(x,h(x,x_1\dots,x_n),x_1,\dots,x_n)
この場合はかなり厄介である
原始再帰定義5
次の原始再帰的関数$ a(y,i)が算術の中に存在すると仮定する.(自己参照になっているので要修正) 自然数の有限列$ x_0,\dots,x_{n-1}のGödel数を$ yとする
$ a(y,i) = x_i
$ a(z,x)=h(x,x_1\dots,x_n)を表しているとすると
$ a(z,0) = h(0,x_1,\dots,x_n) = f(x_1,\dots,x_n)
つまり,$ A_f \lbrack x_1,\dots,x_n,a(z,0)\rbrack
$ a(z,1) = h(0,x_1,\dots,x_n) = g(0,a(z,0),x_1,\dots,x_n)
$ a(z,2) = h(1,x_1,\dots,x_n) = g(1,a(z,1),x_1,\dots,x_n)
$ a(z,x) = h(x-1,x_1,\dots,x_n) = g(x -1,a(z,x-1),x_1\dots,x_n)
つまり,$ A_g \lbrack x-1,a(z,x-1),x_1,\dots,x_n,a(z,x)\rbrack
以上より,$ h(x,x_1,\dots,x_n)=yならば
$ A_f \lbrack x_1,\dots,x_n,a(z,0)\rbrack \land (i < x \to A_g \lbrack x-1,a(z,x-1),x_1,\dots,x_n,a(z,S(i))\rbrack) \land a(x,z)=y
なる$ zが存在して,逆に$ zが存在するなら$ h(x,x_1\dots,x_n) = yを構成できることを意味する
ここまでをまとめると,
$ A_h \lbrack x,x_1,\dots,x_n,y \rbrackを次の式とすると$ hを表現可能.
$ \exists z \left( \begin{array}{l} A_f \lbrack x_1,\dots,x_n,a(z,0)\rbrack \\ {}\land \forall i (i < x \to A_g \lbrack x-1,a(z,x-1),x_1,\dots,x_n,a(z,S(i))\rbrack \\ {}\land a(x,z)=y \end{array} \right)
更に,$ a(z,i) = wを$ E\lbrack z,i,w \rbrackで表すと
$ \exists z \left( \begin{array}{l} \exists w (E\lbrack z,0,w \rbrack \land A_f \lbrack x_1,\dots,x_n,w\rbrack) \\ {}\land \forall i(i < x \to \exists w,\exists w' (E\lbrack z,i,w \rbrack \land E\lbrack z,S(i),w' \rbrack\land A_g \lbrack x-1,w,\dots,x_n,w')\rbrack) \\ {}\land E\lbrack z,x,y\rbrack \end{array} \right)
あとは算術の中で本来ない可能性のある$ E\lbrack z,x,y \rbrackを巧妙に設計する
これは結構面倒なので本を読むこと