$ \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)} \newcommand{\bracket}[1]{\left[\;#1\;\right]} $

形式的体系${\cal R}$を算術化する。

形式的体系${\cal R}$を算術化する。 $\newcommand{\godel}[1]{\left\ulcorner#1\right\urcorner}$
  1. ${\cal R}$の基本記号のゲーデル数
    • 定記号のゲーデル数:
      $\godel{{\mathbf 0}} \equ 3、\godel{^\prime} \equ 5、\godel{\equ} \equ 7$
    • 変数および関数記号のゲーデル数:
      $\godel{a_n} \equ 2^9 \cdot 3^n \quad \left( n \equ 0,1,2,\cdots \right)$
      $\godel{f_n} \equ 2^{11} \cdot 3^n \quad \left( n \equ 0,1,2,\cdots \right)$
  2. 補助記号は構成の順序を示すための記号であるが、以下のゲーデル数の対応のさせ方では、補助記号のゲーデル数を定義する必要は無い。 項や方程式、その他に対応させるゲーデル数は、その構成の順序が分かるように定義されるからである。
  3. 項のゲーデル数
    • $t$が(既にゲーデル数が定義されている)項のとき、
      $\godel{(t)^\prime} \equ 2^5 \cdot 3^{\godel{t}}$
    • $t_1,\cdots,t_n$が(既にゲーデル数が定義されている)項で、$f$が関数記号であるとき、
      $\godel{f(t_1,\cdots,t_n)} \equ 2^{\godel{f}} \cdot 3^{\godel{t_1}} \cdot 5^{\godel{t_2}} \cdot \cdots \cdot p_n^{\godel{t_n}}$
  4. 方程式のゲーデル数
    $t_1,t_2$が(既にゲーデル数の定義されている)項のとき、
    $\godel{t_1 \equ t_2} \equ 2^7 \cdot 3^{\godel{t_1}} \cdot 5^{\godel{t_2}}$
  5. 方程式系のゲーデル数
    $e_1,\cdots,e_l$が(既にゲーデル数の定義されている)方程式であるとき、
    $(e_1,\cdots,e_l) \equ 2^{13} \cdot 3^{\godel{e_1}} \cdot \cdots \cdot p_l^{\godel{e_l}}$
  6. (方程式系$E$からの)演繹のゲーデル数
    • $e$を$E$に含まれる方程式とするとき、演繹$D$が$e$自身ならば、
      $\godel{D} \equ 2^{\godel{e}}$
    • $D_1$を$E$からの演繹とし、$D_1$の最下式を$e_1$とするとき、
      演繹$D$が$e_1$から"代入"の推論規則によって$e_2$を得る$\genfrac{}{}{1pt}{0}{D_1}{e_2}$とすれば、
      $\godel{\genfrac{}{}{1pt}{0}{D_1}{e_2}} \equ 2^{\godel{e_2}} \cdot 3^{\godel{D_1}}$
    • $D_1,D_2$を$E$からの演繹、$e_1$を$D_1$の最下式、$e_2$を$D_2$の最下式とするとき、
      演繹$D$が$e_1$と$e_2$から"置換"の推論規則によって$e_3$を得る$\genfrac{}{}{1pt}{0}{D_1 \quad D_2}{e_3}$とすれば、
      $\godel{\genfrac{}{}{1pt}{0}{D_1 \quad D_2}{e_3}} \equ 2^{\godel{e_3}} \cdot 3^{\godel{D_1}} \cdot 5^{\godel{D_2}}$

以上の算術化によって、${\cal R}$を自然数論の中に埋め込んだとき、${\cal R}$における様々な概念および${\cal R}$で展開される議論を、自然数上の関数、述語として定義し、自然数論の中で展開してみよう。

${\rm N}(x)$ $e$を${\cal R}$における表現とし、$\godel{e} \equ x$とするとき、
"$e$は数項である"ことを自然数論の中で表す述語「$\godel{e}$は数項のゲーデル数である」
を意味する。
以下では、上のような場合、
単に、"$e$は数項である"と「$\cdots$ゲーデル数である」の部分は省略した形で述べる
$\equiv$ $x \equ 3 \lor \left( x \equ 2^5 \cdot 3^{(x)_1} \land {\rm N}((x)_1) \right)$
${\rm V}(x)$ 「$x$は変数記号である」 $\equiv$ $x \equ 2^9 \cdot 3^{(x)_1}$
${\rm FL}(x)$ 「$x$は関数記号である」 $\equiv$ $x \equ 2^{11} \cdot 3^{(x)_1}$
${\rm Tm}(x)$ 「$x$は項である」 $\equiv$ $\begin{array}{@{}c@{}l@{}} & x \equ 3 \\ \lor & {\rm V}(x) \\ \lor & \left( {\rm lh}(x) \equ 2 \land (x)_0 \equ 5 \land {\rm Tm}((x)_1) \right) \\ \lor & \left( {\rm lh}(x) \gt 1 \land {\rm FL}((x)_0) \land (\all i)_{0 \lt i \lt {\rm lh}(x)} {\rm Tm}((x)_i) \right) \end{array}$
${\rm Eq}(x)$ 「$x$は方程式である」 $\equiv$ $\left( x \equ 2^7 \cdot 3^{(x)_1} \cdot 5^{(x)_2} \right) \land {\rm Tm}((x)_1) \land {\rm Tm}((x)_2)$
${\rm SE}(x)$ 「$x$は方程式系である」 $\equiv$ ${\rm lh}(x) \gt 1 \land (x)_0 \equ 13 \land (\all i)_{0 \lt i \lt {\rm lh}(x)} {\rm Eq}((x)_i)$
${\rm Sb}(d, e, t, x)$ 「変数記号$x$に項$t$を代入すると、項あるいは方程式である$e$が$d$になる」 $\equiv$ ${\rm V}(x) \land {\rm Tm}(t) \land$
$\left(\begin{array}{@{}c@{}l@{}} & \left( e \equ x \land d \equ t \right) \\ \lor & \left( \left(\begin{array}{@{}c@{}l@{}} & e \equ 3 \\ \lor & \left( {\rm V}(e) \land e \neq x \right) \end{array}\right) \land d \equ e \right) \\ \lor & \left(\begin{array}{@{}c@{}l@{}} & \left( {\rm Tm}(e) \lor {\rm Eq}(e) \right) \\ \land & {\rm lh}(e) \gt 1 \\ \land & {\rm lh}(e) \equ {\rm lh}(d) \\ \land & (d)_0 \equ (e)_0 \\ \land & (\all i)_{0 \lt i \lt {\rm lh}(e)} {\rm Sb}\left((d)_i, (e)_i, t, x\right) \end{array}\right) \end{array}\right)$
${\rm Ct}(e,x)$ 「項あるいは方程式である$e$が、変数記号$x$を含む」 $\equiv$ $\left( {\rm Tm}(e) \lor {\rm Eq}(e) \right) \land {\rm V}(x) \land \neg {\rm Sb}(e,e,3,x)$
${\rm SC}_n(e,d)$ 「方程式$e$は、方程式$d$から"代入"の推論規則によって得られる」 $\equiv$ ${\rm Eq}(d) \land (\exi x)_{x \lt d} (\exi n)_{n \lt e} \; \left( {\rm N}(n) \land {\rm Ct}(d,x) \land {\rm Sb}(e,d,n,x) \right)$
${\rm RC}_n (e,d,c)$ 「方程式$e$は、方程式$d$と$c$から"置換"の推論規則によって得られる」 $\equiv$ $\begin{array}{@{}c@{}l@{}} & {\rm Eq}(c) \land {\rm FL}((c)_{1,0} \land (\all i)_{0 \lt i \lt {\rm lh}((c)_1)} {\rm N}((c)_{1,i}) \land {\rm N}((c)_2) \\ \land & {\rm Eq}(d) \land (\all x)_{x \lt d} \neg {\rm Ct}(d,x) \land {\rm Eq}(e) \\ \land & (\exi u)_{u \lt d} \left( \begin{array}{@{}c@{}l@{}} & {\rm Tm}(u) \land {\rm Ct}(u, 2^9 \cdot 3) \\ \land & {\rm Sb}((d)_2, u, (c)_1, 2^9 \cdot 3) \\ \land & {\rm Sb}((e)_2, u, (c)_2, 2^9 \cdot 3) \end{array}\right) \end{array}$
※変数記号$a_1$のゲーデル数$\godel{a_1} \equ 2^9 \cdot 3$は、
いかなる関数記号$f_n$のゲーデル数$\godel{f_n} \equ 2^{11} \cdot 3^n$より小さく、
従って、$u \lt d$であるような$u$が取れる事に注意。
${\rm Nu}(z,n)$ 「$z$は自然数$n$に対応する数項である」 $\equiv$ $\left( z \equ 3 \land n \equ 0 \right) \lor \left( z \equ 2^5 \cdot 3^{(z)_1} \land n \neq 0 \land {\rm Nu}((z)_1, n \dot{-} 1) \right)$
${\rm D}(z,y)$ 「$y$は方程式系$z$からの演繹である」 $\equiv$ ${\rm SE}(z) \land \\ \left( \begin{array}{@{}c@{}l@{}} & (\exi i)_{0 \lt i \lt {\rm lh}(z)} \left( y \equ 2^{(z)_i} \right) \\ \lor & \left( y \equ 2^{(y)_0} \cdot 3^{(y)_1} \land {\rm SC}_n ((y)_0, (y)_{1,0}) \land {\rm D}(z, (y)_1) \right) \\ \lor & \left( \begin{array}{@{}l@{}} y \equ 2^{(y)_0} \cdot 3^{(y)_1} \cdot 5^{(y)_2} \land {\rm RC}_n ((y)_0, (y)_{1,0}, (y)_{2,0}) \\ \land {\rm D}(z, (y)_1) \land {\rm D}(z, (y)_2) \end{array} \right) \end{array} \right)$
${\rm S}_n (z,x_1,\cdots,x_n,y)$ 「$z$を方程式系、その主関数記号を$f$とする。
$\overline{x}_1,\cdots,\overline{x}_n$をそれぞれ自然数$x_1,\cdots,x_n$に対応する数項、$\overline{x}$も数項とする。
また、$y$は方程式系$z$からの演繹で、$y$の最下式は、$f({\overline x}_1,\cdots,{\overline x}_n) \equ {\overline x} $の形をしている」
$\equiv$ $\begin{array}{@{}c@{}l@{}} & {\rm D}(z,y) \land {\rm lh}((y)_{0,1}) \equ n+1 \\ \land & {\rm FL}((y)_{0,1,0}) \land (y)_{0,1,0} \equ (z)_{{\rm lh}(z) \dot{-} 1, 1, 0} \\ \land & \left( \begin{array}{@{}c@{}l@{}} & {\rm Nu}((y)_{0,1,1}, x_1) \\ \land & \vdots \\ \land & {\rm Nu}((y)_{0,1,n}, x_n) \\ \land & {\rm N}((y)_{0,2}) \end{array} \right) \end{array}$

$Z$を方程式系としたとき、${\rm S}_n (\godel{Z},x_1,\cdots,x_n,y)$は、

$Z \vdash f(\overline{x}_1,\cdots,\overline{x}_n) \equ \overline{x}$

つまり、$f({\overline x}_1,\cdots,{\overline x}_n) \equ {\overline x}$が$Z$から演繹可能である事を表している。

$\psi_i$は$m_i$変数の関数$(i \equ 1,\cdots,l)$とする。

${\rm D}^{\psi_1,\cdots,\psi_l}(z,y)$ 「$y$は方程式系$z$と$\psi_1,\cdots,\psi_l$に対する関数表からの演繹である」 $\equiv$ ${\rm SE}(z) \land \\ \left( \begin{array}{@{}c@{}l@{}} & (\exi i)_{0 \lt i \lt {\rm lh}(z)} \; ( y \equ 2^{(z)_i} ) \\ \lor & \left( \begin{array}{@{}c@{}l@{}} & y \equ 2^{(y)_0} \land {\rm Eq}((y)_0) \land {\rm FL}((y)_{0,1,0}) \\ \land & \bigvee\limits_{i=1}^l \left( \begin{array}{@{}l@{}} (\exi w_{i,1})_{w_{i,1} \lt y} \; \cdots (\exi w_{i,m_i})_{w_{i,m_i} \lt y} ( \\ \begin{array}{@{}c@{}c@{}l@{}} & & (y)_{0,1} \equ 2^{(y)_{0,1,0}} \cdot 3^{(y)_{0,1,1}} \cdot \cdots \cdot p_{m_i}^{(y)_{0,1,m_i}} \\ & \land & {\rm Nu}((y)_{0,1,1}, w_{i,1}) \\ & \land & \vdots \\ & \land & {\rm Nu}((y)_{0,1,m_i}, w_{i,m_i}) \\ & \land & {\rm Nu}((y)_{0,2}, \psi_i (w_{i,1},w_{i,2},\cdots,w_{i,m_i}) ) \\ \end{array} \\ ) \end{array} \right) \end{array} \right) \\ \lor & \left( y \equ 2^{(y)_0} \cdot 3^{(y)_1} \land {\rm SC}_n ((y)_0, (y)_{1,0}) \land {\rm D}^{\psi_1,\cdots,\psi_l}(z, (y)_1) \right) \\ \lor & \left( \begin{array}{@{}l@{}} y \equ 2^{(y)_0} \cdot 3^{(y)_1} \cdot 5^{(y)_2} \land {\rm RC}_n ((y)_0, (y)_{1,0}, (y)_{2,0}) \\ \land {\rm D}^{\psi_1,\cdots,\psi_l}(z, (y)_1) \land {\rm D}^{\psi_1,\cdots,\psi_l}(z, (y)_2) \end{array} \right) \end{array} \right)$
$S_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,y)$ 「$y$は方程式系$z$と$\psi_1,\cdots,\psi_l$に対する関数表からの演繹で、
$y$の最下式は$f({\overline x}_1,\cdots,{\overline x}_n) \equ {\overline x}$の形をしている。
ただし、$f$は$z$の主関数記号、
${\overline x}_1,\cdots,{\overline x}_n$は、それぞれ自然数$x_1,\cdots,x_n$に対応する数項、${\overline x}$も数項である」
$\equiv$ $\begin{array}{@{}c@{}l@{}} & {\rm D}^{\psi_1,\cdots,\psi_l}(z,y) \land {\rm lh}((y)_{0,1}) \equ n+1 \\ \land & {\rm FL}((y)_{0,1,0}) \land (y)_{0,1,0} \equ (z)_{{\rm lh}(z) \dot{-}1,1,0} \\ \land & \left( \begin{array}{@{}c@{}l@{}} & {\rm Nu}((y)_{0,1,1}, x_1) \\ \land & \vdots \\ \land & {\rm Nu}((y)_{0,1,n}, x_n) \\ \land & {\rm N}((y)_{0,2}) \end{array} \right) \end{array}$
${\rm D}^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,y)$ $\equiv$ ${\rm SE}(z) \land \\ \left( \begin{array}{@{}c@{}l@{}} & (\exi i)_{0 \lt i \lt {\rm lh}(z)} \; ( y \equ 2^{(z)_i} ) \\ \lor & \left( \begin{array}{@{}c@{}l@{}} & y \equ 2^{(y)_0} \land {\rm Eq}((y)_0) \land {\rm FL}((y)_{0,1,0}) \\ \land & \bigvee\limits_{i=1}^l \left( \begin{array}{@{}l@{}} (\exi w_{i,1})_{w_{i,1} \lt y} \; \cdots (\exi w_{i,m_i})_{w_{i,m_i} \lt y} ( \\ \begin{array}{@{}c@{}c@{}l@{}} & & (y)_{0,1} \equ 2^{(y)_{0,1,0}} \cdot 3^{(y)_{0,1,1}} \cdot \cdots \cdot p_{m_i}^{(y)_{0,1,m_i}} \\ & \land & {\rm Nu}((y)_{0,1,1}, w_{i,1}) \\ & \land & \vdots \\ & \land & {\rm Nu}((y)_{0,1,m_i}, w_{i,m_i}) \\ & \land & {\rm Nu}((y)_{0,2}, \textcolor{red}{(v_i)_{w_{i,1},w_{i,2},\cdots,w_{i,m_i}}} ) \\ \end{array} \\ ) \end{array} \right) \end{array} \right) \\ \lor & \left( \begin{array}{@{}l@{}} y \equ 2^{(y)_0} \cdot 3^{(y)_1} \land {\rm SC}_n ((y)_0, (y)_{1,0}) \\ \land \; \textcolor{red}{{\rm D}^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,(y)_1)} \end{array} \right) \\ \lor & \left( \begin{array}{@{}l@{}} y \equ 2^{(y)_0} \cdot 3^{(y)_1} \cdot 5^{(y)_2} \land {\rm RC}_n ((y)_0, (y)_{1,0}, (y)_{2,0}) \\ \land \; \textcolor{red}{{\rm D}^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,(y)_1)} \\ \land \; \textcolor{red}{{\rm D}^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,(y)_2)} \end{array} \right) \end{array} \right)$
${\rm S}_n^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,x_1,\cdots,x_n,y)$ $\equiv$ $\begin{array}{@{}c@{}l@{}} & {\rm D}^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,y) \land {\rm lh}((y)_{0,1}) \equ n+1 \\ \land & {\rm FL}((y)_{0,1,0}) \land (y)_{0,1,0} \equ (z)_{{\rm lh}(z) \dot{-}1,1,0} \\ \land & \left( \begin{array}{@{}c@{}l@{}} & {\rm Nu}((y)_{0,1,1}, x_1) \\ \land & \vdots \\ \land & {\rm Nu}((y)_{0,1,n}, x_n) \\ \land & {\rm N}((y)_{0,2}) \end{array} \right) \end{array}$

表記の都合上

$\prod\limits_{i \lt n} p_i \; {\rm exp} \; a_i :\equiv \prod\limits_{i \lt n} p_i^{a_i}$

と置く。

原始帰納的関数$\varphi(x_1,\cdots,x_n)$に対して、原始帰納的関数${\tilde \varphi}(x_1,\cdots,x_n)$を

${\tilde \varphi}(x_1,\cdots,x_n) \equ \prod\limits_{i_1 \lt x_1} p_{i_1} {\rm exp}( \cdots ( \prod\limits_{i_n \lt x_n} p_{i_n} {\rm exp} \; \varphi(i_1,\cdots,i_n) ) \cdots )$

で定義する。この定義から明らかに、$a_i \lt x_i \; (i \equ 1,\cdots,n)$ に対して、

$\varphi(a_1,\cdots,a_n) \equ ( {\tilde \varphi}(x_1,\cdots,x_n) )_{a_1,\cdots,a_n}$

が成り立つ。

${\rm S}_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,y)$は、$(n+2)$変数の述語であり、$\psi_1,\cdots,\psi_l$で原始帰納的であるのに対し、
${\rm S}_n^{m_1,\cdots,m_l}(v_1,\cdots,v_l,z,x_1,\cdots,x_n,y)$は、$(l+n+2)$変数の原始帰納的述語である。

${\rm S}_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,y)$は、無限集合である関数表$E_{g_1,\cdots,g_l}^{\psi_1,\cdots,\psi_l}$によって定められているのに対し、
${\rm S}_n^{m_1,\cdots,m_l}({\tilde \psi}_1(v,\cdots,v),\cdots,{\tilde \psi}_l(v,\cdots,v),z,x_1,\cdots,x_n,y)$は、有限の表${\tilde \psi}_1(v,\cdots,v),\cdots,{\tilde \psi}_l(v,\cdots,v)$で定義されている事に注意。

関数$\psi_i$は$m_i$変数の関数$(i \equ 1,\cdots,l)$とする。
${\rm T}_n(z,x_1,\cdots,x_n,y)$ $:\equiv$
${\rm S}_n(z,x_1,\cdots,x_n,y)$
$\land \all t \lt y \; \neg {\rm S}_n(z,x_1,\cdots,x_n,t)$
${\rm T}_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,y)$ $:\equiv$
${\rm S}_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,y)$
$\land \all t \lt y \; \neg {\rm S}_n^{\psi_1,\cdots,\psi_l}(z,x_1,\cdots,x_n,t)$
${\rm T}_n^{m_1,\cdots,m_l}({\tilde \psi}_1(y,\cdots,y),\cdots,{\tilde \psi}_l(y,\cdots,y),z,x_1,\cdots,x_n,y)$ $:\equiv$
${\rm S}_n^{m_1,\cdots,m_l}({\tilde \psi}_1(y,\cdots,y),\cdots,{\tilde \psi}_l(y,\cdots,y),z,x_1,\cdots,x_n,y)$
$\land \all t \lt y \; \neg {\rm S}_n^{m_1,\cdots,m_l}({\tilde \psi}_1(t,\cdots,t),\cdots,{\tilde \psi}_l(t,\cdots,t),z,x_1,\cdots,x_n,t)$