$ \newcommand{\exi}{\exists\,} \newcommand{\all}{\forall} \newcommand{\equ}{\!=\!} \newcommand{\nequ}{\!\neq\!} \newcommand{\amp}{\;\&\;} \renewcommand{\Set}[2]{\left\{\;#1\mathrel{}\middle|\mathrel{}#2\;\right\}} \newcommand{\parenth}[1]{\left(\;#1\;\right)} $

${\rm S}_n^m$-定理を自分なりに纏める。

$\newcommand{\godel}[1]{\left\ulcorner#1\right\urcorner}$ $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$とする。
この時、原始帰納的関数$\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]$ である。
証明終