${\rm S}_n^m$-定理を自分なりに纏める。
$\lambda y_1 \cdots y_m x_1 \cdots x_n \; f(y_1,\cdots,y_m,x_1,\cdots,x_n)$を$(m+n)$-変数の帰納的な部分関数とする。
この関数$f$のゲーデル数を$e$とする。
この関数$f$のゲーデル数を$e$とする。
この時、原始帰納的関数$\lambda z y_1 \cdots y_m \; S_n^m(z,y_1,\cdots,y_m)$が存在して、任意の$y_1,\cdots,y_m$に対し、
$\lambda x_1 \cdots x_n \left[ \{e\}(y_1,\cdots,y_m,x_1,\cdots,y_n) \simeq \{ S_n^m(e,y_1,\cdots,y_m) \}(x_1,\cdots,x_n) \right]$
が成り立つ。証明
- $m \equ 0$の場合は、${\rm S}_n^0(z) \equ z$ とすればよい。$m \geq 1$とする。
- 表記を簡単にするために、$x_1,\cdots,x_n$ を ${\boldsymbol x}$ で表す。
自然数の列$x_1,\cdots,x_n$にそれぞれ対応する数項の列${\overline x}_1,\cdots,{\overline x}_n$ を ${\overline {\boldsymbol x}}$ で表す。
$y_1,\cdots,y_m$についても同様である。 - $\varphi(z,{\boldsymbol y},{\boldsymbol x}) :\equiv {\rm U}(\mu w {\rm T}_{m+n}(z,{\boldsymbol y},{\boldsymbol x},w))$ と置く。
- $\varphi$は帰納的部分関数、従って、形式的に計算可能なので、方程式系$D$が存在して、任意の$z,{\boldsymbol y},{\boldsymbol x}, v$ に対して、
$D \vdash g({\overline z},{\overline {\boldsymbol y}}, {\overline {\boldsymbol x}}) \equ {\overline v} \Leftrightarrow \varphi(z, {\boldsymbol y}, {\boldsymbol x}) \equ v$が成り立つ。ただし、$g$は$D$の主関数記号である。
- $h$を$D$に含まれない関数記号とする。
- $z,{\boldsymbol y}$ に対し、方程式系$E_{z, {\boldsymbol y}}$ を $D, h(a_1,\cdots,a_n) \equ g({\overline z}, {\overline {\boldsymbol y}}, a_1,\cdots,a_n)$ とし、
$S_n^m(z, {\boldsymbol y}) :\equiv \godel{ E_{z, {\boldsymbol y}} }$ と定義する。 - $S_n^m(z, {\boldsymbol y}) \equ \godel{D} * 2^{\godel{h(a_1,\cdots,a_n) \equ g({\overline z}, {\overline {\boldsymbol y}}, a_1,\cdots,a_n)}} \equ$
${\LARGE \godel{D} * 2^{ 2^{\godel{\equ}} \cdot 3^{\godel{h(a_1,\cdots,a_n)}} \cdot 5^{\godel{g({\overline z}, {\overline {\boldsymbol y}}, a_1,\cdots,a_n)}} }}$なので、原始帰納的関数である事が分かる(自然数$k$に対して$\godel{{\overline k}}$を求める関数は原始帰納的である)。 - ${\boldsymbol y}$ を任意にとって固定しておく。
- φが形式的に計算可能より、任意の${\boldsymbol x}, v$に対して、
$E_{e, {\boldsymbol y}} \vdash h({\overline {\boldsymbol x}}) \equ {\overline v} \Leftrightarrow \varphi(e, {\boldsymbol y}, {\boldsymbol x}) \equ v$が成り立つ。 - 従って、定義により、$\lambda {\boldsymbol x} \left[ \; {\rm U}(\mu w {\rm T}_n ( S_n^m(e, {\boldsymbol y}), {\boldsymbol x}, w ) ) \simeq \varphi(e, {\boldsymbol y}, {\boldsymbol x}) \; \right]$ が成り立つ(${\boldsymbol y}$に応じて存在する方程式系が変わるので、$\lambda {\boldsymbol x}$となるのだ)。
- また、帰納的部分関数$\lambda {\boldsymbol x} {\rm U}(\mu w {\rm T}_n ( S_n^m(e, {\boldsymbol y}), {\boldsymbol x}, w ) )$ のゲーデル数は明らかに ${\rm S}_n^m(e, {\boldsymbol y})$ なので、
$\lambda {\boldsymbol x} \left[ \; \{ {\rm S}_n^m (e, {\boldsymbol y}) \}({\boldsymbol x}) \simeq {\rm U}(\mu w {\rm T}_n ( S_n^m(e, {\boldsymbol y}), {\boldsymbol x}, w ) ) \; \right]$である。 - そして、$\varphi(z, {\boldsymbol y}, {\boldsymbol x})$ と $e$ の定義より、
$\lambda \left[ \; \varphi(e, {\boldsymbol y}, {\boldsymbol x} ) \simeq \{e\}({\boldsymbol y}, {\boldsymbol x}) \; \right]$である。 - 以上より、$\lambda {\boldsymbol x} \left[ \; \{ {\rm S}_n^m (e, {\boldsymbol y}) \}({\boldsymbol x}) \simeq \{e\}({\boldsymbol y}, {\boldsymbol x}) \; \right]$ である。