形式的体系${\cal R}$を算術化する。
- ${\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)$
- 定記号のゲーデル数：
- 補助記号は構成の順序を示すための記号であるが、以下のゲーデル数の対応のさせ方では、補助記号のゲーデル数を定義する必要は無い。 項や方程式、その他に対応させるゲーデル数は、その構成の順序が分かるように定義されるからである。
- 項のゲーデル数
- $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}}$
- $t$が(既にゲーデル数が定義されている)項のとき、
- 方程式のゲーデル数
$t_1,t_2$が(既にゲーデル数の定義されている)項のとき、
$\godel{t_1 \equ t_2} \equ 2^7 \cdot 3^{\godel{t_1}} \cdot 5^{\godel{t_2}}$ - 方程式系のゲーデル数
$e_1,\cdots,e_l$が(既にゲーデル数の定義されている)方程式であるとき、
$\godel{(e_1,\cdots,e_l)} \equ 2^{13} \cdot 3^{\godel{e_1}} \cdot \cdots \cdot p_l^{\godel{e_l}}$ - (方程式系$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}}$
- $e$を$E$に含まれる方程式とするとき、演繹$D$が$e$自身ならば、
以上の算術化によって、${\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)$ |
|
