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

帰納的関数論 3:自然数論の形式的体系${\cal P}$

自然数論の形式的体系${\cal P}$を定義する。
  1. 記号
    • 対象記号:${\mathbf 0}$
    • 関数記号:$^\prime$
    • 論理記号:$\neg$、$\lor$、$\all$
    • 補助記号:$($、$)$
    • 変数記号:おのおのの型ごとに、それぞれ可算個無限個ずつの変数を用意する。
      • $1$階のタイプの変数記号:$x_1$、$y_1$、$z_1$、$\cdots$

        これは、${\mathbf 0}$を含む自然数全体上の変数を表す記号である。

      • $2$階のタイプの変数記号:$x_2$、$y_2$、$z_2$、$\cdots$

        これは、自然数上で定義された1変数の述語を表す。

      • …:…
      • $n$階のタイプの変数記号:$x_n$、$y_n$、$z_n$、$\cdots$
      • $n+1$階のタイプの変数記号:$x_{n+1}$、$y_{n+1}$、$z_{n+1}$、$\cdots$

        これは、$n$階のタイプの対象のクラスに対する変数を表す。

      • …:…
  2. 項(term)
    1. 対象記号${\mathbf 0}$は1階のタイプの項である。
    2. 1階のタイプの変数記号は1階のタイプの項である。
    3. ${\mathbf t}$が1階のタイプの項である時、${\mathbf t}^\prime$は1階のタイプの項である。
      (${\mathbf 0}, {\mathbf 0}^\prime, {\mathbf 0}^{\prime\prime}, \cdots,$ を特に、数項(numeral)と呼ぶ。)
    4. 以上によって定義されるもののみが1階のタイプの項である。
    5. $1 \lt n$の時、$n$階のタイプの項とは$n$階のタイプの変数記号のことである。
    6. 以上によって定義される各階のタイプの項のみが項である。
  3. 論理式(formula)
    1. ${\mathbf s}$が$n+1$階のタイプの項で、${\mathbf t}$が$n$階のタイプの項である時、${\mathbf s} ( {\mathbf t} )$は論理式である。
      特に、このような論理式を基本論理式(prime formula、atomic formula)と呼ぶ。
    2. ${\mathbf A}$が論理式である時、$\neg ( {\mathbf A} )$は論理式である。
    3. ${\mathbf A, B}$が論理式である時、$( {\mathbf A} ) \lor ( {\mathbf B} )$は論理式である。
    4. ${\mathbf A}$が論理式で${\mathbf x}$が($n$階のタイプの)変数記号である時、$\all {\mathbf x} ( {\mathbf A} )$は論理式である。
    5. 以上によって定義されるもののみが論理式である。
  4. 束縛変数、自由変数
    論理式$\all {\mathbf x} ( {\mathbf A} )$においては、変数${\mathbf x}$は束縛されているという。
    別の論理式${\mathbf B}$の一部分として$\all {\mathbf x} ( {\mathbf A} )$という論理式が現れる場合にも、「$\all {\mathbf x} ( {\mathbf A} )$という部分において変数${\mathbf x}$は束縛されている」という。
    従って、1つの論理式${\mathbf B}$の中においても、同じ変数${\mathbf x}$が、ある場所においては束縛され、ある場所においては束縛されていない、ということはあり得る。
    束縛されている変数を束縛変数という。
    束縛されていない変数を自由変数という。
    束縛変数とか自由変数とかは、論理式中の各場所における各変数の用いられ方についての名称と考えなければならない
  5. 補助記号の省略と追加
    誤解の恐れが無い場合には、論理式$\neg({\mathbf A}), ( {\mathbf A} ) \to ( {\mathbf B} ), \all {\mathbf x} ( {\mathbf A} )$などを単に$\neg {\mathbf A}, {\mathbf A} \to {\mathbf B}, \all {\mathbf x} {\mathbf A}$などと書き表す。
    また、読みやすくするため、$(,)$の代わりに$[,]$や$\{,\}$をも適宜使用する。
  6. 補助的論理記号
    • 論理式$( {\mathbf A} ) \land ( {\mathbf B} )$を$\neg ( ( \neg ( {\mathbf A} ) ) \lor ( \neg ( {\mathbf B} ) ) )$で定義する。
    • 論理式$( {\mathbf A} ) \Rightarrow ( {\mathbf B} )$を$( \neg ( {\mathbf A} ) ) \lor ( {\mathbf B} )$で定義する。
    • 論理式$\exi {\mathbf x}( {\mathbf A} )$を$\neg ( \all {\mathbf x} ( \neg ( {\mathbf A} ) ) )$で定義する。
    • 論理式$( {\mathbf A} ) \Leftrightarrow ( {\mathbf B} )$を$( ( {\mathbf A} ) \Rightarrow ( {\mathbf B} ) ) \land ( ( {\mathbf B} ) \Rightarrow ( {\mathbf A} ) )$で定義する。
    • 論理式${\mathbf s} \equ {\mathbf t}$を$\all x_{n+1} \parenth{ (x_{n+1}({\mathbf s})) \Rightarrow (x_{n+1}({\mathbf t}))}$で定義する。
      ただし、${\mathbf s,t}$は$n$階のタイプの項である。
  7. 論理式の自由変数への代入
    論理式の中の自由変数を、それと同じ階数を持つ項で置き換えれば、再び論理式が得られる。
    論理式${\mathbf A}$ と 同じ階数の変数${\mathbf x}$ならびに項${\mathbf t}$が与えられた時、${\mathbf A}$の中に自由変数として現れている全ての${\mathbf x}$を${\mathbf t}$で置き換えて得られる論理式を
    ${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$
    と表し、${\mathbf A}$から${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$を作ることを、${\mathbf A}$の中の${\mathbf x}$に${\mathbf t}$を代入(substitute)するという。
    論理式${\mathbf A}$から${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$を作る場合、${\mathbf A}$に現れる自由変数${\mathbf x}$に着目するという意味で、${\mathbf A}$を${\mathbf F}({\mathbf x})$というような記法で表し、${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$を${\mathbf F}({\mathbf t})$と略記することがある。
    ${\mathbf F}({\mathbf x})$が${\mathbf x}$を自由変数として含んでいない時は、${\mathbf F}({\mathbf t})$は${\mathbf F}({\mathbf x})$そのものである。
  8. 代入についての付帯条件
    論理式${\mathbf A}$から${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$を作る代入においては、新たに束縛変数の個数が増加することがあってはならない
    以後、特に断らなくても、付帯条件は自動的に満たされているものとする。
  9. 公理
    1. 自然数の公理
      1. $\neg ( x_1^\prime \equ {\mathbf 0} )$
      2. $x_1^\prime \equ y_1^\prime \Rightarrow x_1 \equ y_1$
      3. $\bracket{ x_2({\mathbf 0}) \land \all x_1 \parenth{ x_2(x_1) \Rightarrow x_2(x_1^\prime) } } \Rightarrow \all x_1 \parenth{ x_2(x_1) }$
    2. 命題論理の公理
        ${\mathbf A, B, C}$は任意の論理式とする。
      1. $\parenth{ {\mathbf A} \lor {\mathbf A} } \Rightarrow {\mathbf A}$
      2. ${\mathbf A} \Rightarrow \parenth{ {\mathbf A} \lor {\mathbf B} }$
      3. $\parenth{ {\mathbf A} \lor {\mathbf B} } \Rightarrow \parenth{ {\mathbf B} \lor {\mathbf A} }$
      4. $\parenth{{\mathbf A} \Rightarrow {\mathbf B} } \Rightarrow \bracket{ \parenth{ {\mathbf C} \lor {\mathbf A} } \Rightarrow \parenth{ {\mathbf C} \lor {\mathbf B} } }$
    3. 述語論理の公理
        ${\mathbf A}, {\mathbf B}$は任意の論理式とする。
      1. $\all {\mathbf x} ( {\mathbf A} ) \Rightarrow {\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$
        ただし、項${\mathbf t}$は変数${\mathbf x}$と同じ階数を持つ任意の項で、${\rm Subst}\;{\mathbf A}{\displaystyle{{\mathbf x} \choose {\mathbf t} }}$を作る時に付帯条件は満たされているとする。
      2. $\all {\mathbf x} \parenth{ {\mathbf B} \lor {\mathbf A} } \Rightarrow \parenth{ {\mathbf B} \lor \all {\mathbf x} ( {\mathbf A} ) }$
        ただし、論理式${\mathbf B}$は変数${\mathbf x}$を自由変数として含まないものとする。
    4. 内包の公理
      • $\exi {\mathbf y} \bracket{ \all {\mathbf x} \parenth{ {\mathbf y}( {\mathbf x} ) \Leftrightarrow {\mathbf A} } }$
        ただし、変数${\mathbf x}$は$n$階のタイプの変数記号、変数${\mathbf y}$は$n+1$階のタイプの変数記号とし、論理式${\mathbf A}$は変数${\mathbf y}$を自由変数として含まないとする。
    5. 外延性の公理
      • $\all {\mathbf w} \parenth{ {\mathbf x}( {\mathbf w} ) \Leftrightarrow {\mathbf y}( {\mathbf w} ) } \Rightarrow {\mathbf x} \equ {\mathbf y}$
        ただし、変数${\mathbf w}$は$n$階のタイプの変数記号、変数${\mathbf x, y}$は$n+1$階のタイプの変数記号とする。
  10. 証明
    1. 個々の公理は全て証明出来る論理式である。
    2. ${\mathbf A}, {\mathbf A} \to {\mathbf B}$の両方が証明出来る論理式ならば、${\mathbf B}$も証明出来る論理式である。
    3. ${\mathbf A}$が証明出来る論理式ならば、任意の変数${\mathbf x}$に対して、$\all {\mathbf x} {\mathbf A}$も証明出来る論理式である。
    4. 以上によって定義されるもののみが証明出来る論理式である。
    論理式${\mathbf A}$が証明出来ることを
    $\vdash {\mathbf A}$
    と表す。
以上によって、形式的体系${\cal P}$は定められた。
形式的体系${\cal P}$を算術化する。

形式的体系${\cal P}$における形式的対象全体${\rm Obj}$は可算無限の濃度なので、各対象には自然数を対応させることが出来る。その対応$\godel{\;} : {\rm Obj} \to {\mathbb N}, x \mapsto \godel{x}$を次の条件を満たすようにして定義する。$\godel{x}$を$x$のゲーデル数という。

  1. $x \parenth{ \in {\rm Obj} }$に対し、$\godel{x} \parenth{ \in {\mathbb N} }$の値を計算する有限の手続きが、実際に定められている。
  2. 任意に$y \parenth{ \in {\mathbb N} }$をとった時、$x \parenth{ \in {\rm Obj} }$が存在して、$\godel{x} \equ y$が成り立つかどうか、成り立つならば、その$x$がどのようなものであるかを決定する有限の手続きが、実際に定められている。
  3. $\godel{\;}$は単射である。

この$\godel{\;}$により、${\cal P}$における対象$x$と$y$との関係${\mathbf R}(x, y)$は、${\mathbb N}$における自然数$\godel{x}$と$\godel{y}$との述語$R(\godel{x}, \godel{y})$と考えることが出来るので、${\cal P}$における議論と、それに対応する${\mathbb N}$での議論は等価なものと言える。

${\cal P}$における議論を${\mathbb N}$におけるある種の算術に置き換える、${\cal P}$の算術化は、次の効用を持ち、不完全性定理の証明の本質的な部分をなす。

  1. 異なったタイプの変数記号などのように、異なったレベルの概念を一様に${\mathbb N}$の中に表現できる。
  2. 様々な理論、様々な対象の多様性を自然数の中で統一して議論し、比較することができる。

  1. ${\cal P}$の記号のゲーデル数
    • $\godel{{\mathbf 0}} :\equ 1, \godel{\prime} :\equ 3, \godel{\neg} :\equ 5, \godel{\lor} :\equ 7, \godel{\all} :\equ 9, \godel{(} :\equ 11, \godel{)} :\equ 13$
    • $\godel{x_n} :\equ 17^n, \godel{y_n} :\equ 19^n, \godel{z_n} :\equ 23^n, \cdots$
  2. $e_0, e_1, \cdots, e_k$が既にゲーデル数が定義されている対象の列の時、
    $\godel{e_0 e_1 \cdots e_k} :\equ 2^{\godel{e_0}} \cdot 3^{\godel{e_1}} \cdot \cdots \cdot p_k^{\godel{e_k}}$

形式的体系${\cal P}$における概念を、直観的自然数論上の関数や述語として、定義し表現する。

$P(x_1, \cdots, x_n, y)$を述語とする。
$(\varepsilon y)_{y \lt z} P(x_1, \cdots, x_n, y) :\equ \left\{\begin{array}{@{}l@{}r@{}} (\mu y)_{y \lt z} P(x_1, \cdots, x_n, y) & \parenth{ \exi y \lt z \; P(x_1, \cdots, x_n, y) {\rm の時} } \\ 0 & \parenth{ \neg \exi y \lt z \; P(x_1, \cdots, x_n, y) {\rm の時} } \end{array}\right.$
$(\varepsilon y)_{y \lt z} P(x_1, \cdots, x_n, y) {\rm は}\braces{ P }{\text -}{\rm 原始帰納的関数}$ が成り立つ。

以下の関数、述語は全て原始帰納的である。
${\rm Seq}^{n+1}(x_0, \cdots, x_n)$ $x_i$が${\cal P}$での表現$e_i \parenth{ i \equ 0, \cdots, n }$の時、
表現$e_0 \cdots e_n$を表すゲーデル数$\godel{ e_0 \cdots e_n }$を求める関数
以下、単に「表現$e_0 \cdots e_n$のゲーデル数」等と簡略して述べる。
$:\equ$ $2^{x_0} \cdot \cdots \cdot p_n^{x_n}$
${\rm Par}(x)$ 「表現$(e)$のゲーデル数」 $:\equ$ ${\rm Seq}^1(11) \ast x \ast {\rm Seq}^1(13)$
${\rm Var}(n, x)$ 「自然数$x$は$n$階のタイプの変数記号のゲーデル数である」事を意味する述語 $:\Leftrightarrow$ $\exi y_{13 \lt y \leq x} \bracket{ {\rm pr}(y) \land x \equ y^n } \land n \neq 0$
${\rm Var}(x)$ 「自然数$x$は変数記号のゲーデル数である」 $:\Leftrightarrow$ $\exi n_{n \lt x} \bracket{ {\rm Var}(n, x) }$
${\rm Neg}(x)$ 「表現$\neg (e)$のゲーデル数」 $:\equ$ ${\rm Seq}^1(5) \ast {\rm Par}(x)$
${\rm Dis}(x, y)$ 「表現$(e_1) \lor (e_2)$のゲーデル数」 $:\equ$ ${\rm Par}(x) \ast {\rm Seq}^1(7) \ast {\rm Par}(y)$
${\rm Gen}(x, y)$ 「表現$\all e_1(e_2)$のゲーデル数」 $:\equ$ ${\rm Seq}^1(9) \ast {\rm Seq}^1(x) \ast {\rm Par}(y)$
${\rm Suc}(x, n)$ 「表現$e^{\overbrace{\prime \cdots \prime}^{n}}$のゲーデル数」    
${\rm Suc}(x, 0)$ $:\equ$ $x$
${\rm Suc}(x, n+1)$ $:\equ$ ${\rm Suc}(x, n) \ast {\rm Seq}^1(3)$
${\rm Z}(n)$ 「数項${\mathbf 0}^{\overbrace{\prime \cdots \prime}^{n}}$のゲーデル数 $:\equ$ ${\rm Suc}({\rm Seq}^1(1), n)$
${\rm Ter}_1(x)$ 「$x$は1階のタイプの項のゲーデル数である」 $:\Leftrightarrow$ $\exi m_{m \lt x} \exi n_{n \lt x} \bracket{\begin{array}{@{}c@{}l@{}} & \parenth{ m \equ 1 \lor {\rm Var}(1, m) } \\ \land & x \equ {\rm Suc}({\rm Seq}^1(m), n) \end{array}}$ $x$は、「${\mathbf 0}$か1階のタイプの変数記号に
$n$個の$\prime$を連接させた文字列」
のゲーデル数
${\rm Typ}(n, x)$ 「$x$は$n$階のタイプの項のゲーデル数」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & \bracket{ n \equ 1 \land {\rm Ter}_1(x) } \\ \lor & 1 \lt n \land \exi y_{y \lt x} \bracket{ {\rm Var}(n, y) \land x \equ {\rm Seq}^1(y) } \end{array}\right.$
${\rm Te}(n, x)$ 「$e$に含まれる全ての変数記号のタイプを
$n$階上げて得られる表現のゲーデル数」
$:\equ$ $(\varepsilon y)\left\{\begin{array}{@{}c@{}l@{}} & y \lt x^\parenth{ x^n } \\ \land & \all k_{k \lt {\rm lh}(x)} \left\{\begin{array}{@{}c@{}l@{}} & (x)_k \leq 13 \land (y)_k \equ (x)_k \\ \lor & \left(\begin{array}{@{}c@{}l@{}} & 13 \lt (x)_k \\ \land & (y)_k \equ (x)_k \cdot \bracket{ (\varepsilon z)_{z \lt x} \parenth{ {\rm pr}(z) \land z | (x)_k } }^n \end{array}\right. \end{array}\right. \end{array}\right.$ "文字列$x$"に対して1文字づつ捜査していく。
$k$番目の文字が変数記号でない時はそのまま。
変数記号の時は冪指数$(x)_k$は$p_i^m$の形なので、
$p_i^m \cdot p_i^n \equ p_i^{m+n}$にする。
また、$(x)_k \cdot \bracket{ (\varepsilon z)_{z \lt x} \parenth{ {\rm pr}(z) \land z | (x)_k } }^n \lt (x)_k \cdot x^n$
と$x \equ {\displaystyle \prod\limits_{k \lt {\rm lh}(x)}} p_k^{(x)_k}$を合わせると
求める$y$は$y \lt x^{x^n}$を満たす。
${\rm Elf}(x)$ 「$x$は基本論理式のゲーデル数である」 $:\Leftrightarrow$ $\exi y_{y \lt x} \; \exi z_{z \lt x} \; \exi n_{n \lt x} \;\bracket{ {\rm Typ}(n, y) \land {\rm Typ}(n+1, z) \land x \equ z \ast {\rm Par}(y) }$
${\rm Op}(x, y, z)$ $e_1, e_2, e_3$が論理式である時、
「$e_1$は、$e_2$あるいは$e_2, e_3$から構成される(論理式である)」
$:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & \parenth{ x \equ {\rm Neg}(y) } \\ \lor & \parenth{ x \equ {\rm Dis}(y, z) } \\ \lor & \exi w_{w \lt x} \parenth{ {\rm Var}(w) \land x \equ {\rm Gen}(w, y) } \end{array}\right.$
${\rm FR}(x)$ $e_0, \cdots, e_l$が論理式で、かつ、
$x \equ {\rm Seq}^{l+1}(\godel{e_0}, \cdots, \godel{e_l})$である時、
「$e_0, \cdots, e_l$は"論理式の構成系列"である」
$:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & 0 \lt {\rm lh}(x) \\ \land & \all i_{i \lt {\rm lh}(x)} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Elf}( (x)_i ) \\ \lor & \exi j_{j \lt i} \exi k_{k \lt i} {\rm Op}( (x)_i, (x)_j, (x)_k ) \end{array}\right. \end{array}\right.$
${\rm Form}(x)$ 「$x$は論理式のゲーデル数である」 $:\Leftrightarrow$ $\exi n \bracket{ n \lt ( p_{{\rm lh}(x)^2}^{x \cdot {\rm lh}(x)^2} ) \land {\rm FR}(n) \land x \equ (n)_{{\rm lh}(n) \dot{-} 1 } }$ $x \equ \godel{e}, n \equ {\rm Seq}^{k+1}(\godel{e_0}, \cdots, \godel{e_k})$とする。
$e_i$は$e$の部分論理式なので$\godel{e_i} \lt \godel{e}$。
従って、$p_i^\godel{e_i} \lt p_i^\godel{e}$。
$k \lt {\rm lh}(x)^2$が示せれば$n \lt ( p_{{\rm lh}(x)^2}^{x \cdot {\rm lh}(x)^2} )$が分かるのだが…
${\rm B}(v, n, x)$ $x \equ \godel{e}, v \equ \godel{s}$の時、
「論理式$e$の$n$番目の表現は、変数記号$s$で束縛されている。」
$:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & {\rm Var}(v) \land {\rm Form}(x) \\ \land & \exi a_{a \lt x} \; \exi b_{b \lt x} \; \exi c_{c \lt x} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Form}(b) \\ \land & x \equ a \ast \parenth{ {\rm Gen}(v, b) } \ast c \\ \land & {\rm lh}(a) \lt n \leq {\rm lh}(a) + {\rm lh}({\rm Gen}(v, b)) \end{array}\right. \end{array}\right.$
${\rm Fr}(v, n, x)$ $x \equ \godel{e}, v \equ \godel{s}$の時、
「論理式$e$の$n$番目の表現は、変数記号$s$であり、自由変数である。」
$:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & {\rm Var}(v) \land {\rm Form}(x) \\ \land & v \equ (x)_n \land n \lt {\rm lh}(x) \\ \land & \neg ( {\rm B}(v, n, x) ) \end{array}\right.$
${\rm Fr}(v, x)$ $x \equ \godel{e}, v \equ \godel{s}$の時、
「論理式$e$の中に、自由変数記号$s$が現れる。」
$:\Leftrightarrow$ $\exi n_{n \lt {\rm lh}(x)} ( {\rm Fr}(v, n, x) )$
${\rm Sub}\;x{\displaystyle{ n \choose y}}$ $x \equ \godel{e_0 \cdots e_m}, y \equ \godel{f}$の時、
「表現$e_0 \cdots e_m$の中の$e_n$を表現$f$で置き換えて得られる表現のゲーデル数」
$:\equ$ $(\varepsilon z) \left\{\begin{array}{@{}c@{}l@{}} & z \leq p_{{\rm lh}(x)+{\rm lh}(y)}^{x+y} \\ \land & \exi u_{u \lt x} \; v_{v \lt x} \;\left\{\begin{array}{@{}c@{}l@{}} & x \equ u \ast {\rm Seq}^1( (x)_n ) \ast v \\ \land & z \equ u \ast y \ast v \\ \land & n \equ {\rm lh}(u) \end{array}\right. \end{array}\right.$ なぜ$z \leq p_{{\rm lh}(x)+{\rm lh}(y)}^{x+y}$でいいのか
分からない。
${\rm St}(k, v, x)$ $v \equ \godel{s}, x \equ \godel{e}$の時、
「変数記号$s$が論理式$e$に何回自由に現れているかを左から見ていった時、
丁度$n$文字目で第$k+1$回目の自由な現れになっている。そんな$n$」
   
${\rm St}(0, v, x)$ $:\equ$ $(\varepsilon n)_{n \lt {\rm lh}(x)} \left\{\begin{array}{@{}c@{}r@{}} & {\rm Fr}(v, n, x) \\ \land & \neg \exi p_{p \lt n} {\rm Fr}(v, p, x) \end{array}\right.$
${\rm St}(k+1, v, x)$ $:\equ$ $(\varepsilon n)_{n \lt {\rm lh}(x)} \left\{\begin{array}{@{}c@{}r@{}} & {\rm St}(k, v, x) \lt n \\ \land & {\rm Fr}(v, n, x) \\ \land & \neg \exi p_{{\rm St}(k, v, x) \lt p \lt n} {\rm Fr}(v, p, x) \end{array}\right.$
${\rm A}(v, x)$ $s$は変数記号、$e$は論理式、$v \equ \godel{s}, x \equ \godel{e}$の時、
「$e$に現れる自由変数記号$s$の個数$k$」
$:\equ$ $(\varepsilon k)_{k \lt {\rm lh}(x)} \; {\rm St}(k, v, x) \equ 0$
${\rm Sb}_k \!\left( x \; \displaystyle{v \atop y} \right)$ $e$は論理式、$s$は変数記号、$x \equ \godel{e}, v \equ \godel{s}, y \equ \godel{f}$の時、
「論理式$e$に自由に現れる左から$k$個分の変数記号$s$を
表現$f$で置き換えて得られる表現のゲーデル数」
   
${\rm Sb}_0 \!\left( x \; \displaystyle{v \atop y} \right)$ $:\equ$ $x$
${\rm Sb}_{k+1} \!\left( x \; \displaystyle{v \atop y} \right)$ $:\equ$ ${\rm Sub}\!\left[ {\rm Sb}_k \!\left( x \; \displaystyle{v \atop y} \right) \right]\!{\displaystyle{ {\rm St}(k, v, x) \choose y }}$
${\rm Sb}\!\left( x \; \displaystyle{v \atop y} \right)$ $e$は論理式、$s$は変数記号、$x \equ \godel{e}, v \equ \godel{s}, y \equ \godel{f}$の時、
「論理式$e$に自由に現れる全ての変数記号$s$を
表現$f$で置き換えて得られる表現のゲーデル数」
$:\equ$ ${\rm Sb}_{A(v, x)} \!\!\left( x \; \displaystyle{v \atop y} \right)$

${\rm Sb}\!\left( x \ \displaystyle{v \ w \atop y \ z} \right)$ $:\equ$ ${\rm Sb}\!\left[ {\rm Sb}\!\left( x \ \displaystyle{ v \atop y } \right) \! \displaystyle{ w \atop z } \right]$
${\rm Sb}\!\left( x \ \displaystyle{ u_1 \ u_2 \cdots u_n \atop y_1 \ y_2 \cdots y_n} \right)$ $:\equ$ ${\rm Sb}\!\left[ {\rm Sb}\!\left( x \ \displaystyle{ u_1 \ u_2 \cdots u_{n-1} \atop y_1 \ y_2 \cdots y_{n-1}} \right) \! \displaystyle{u_n \atop y_n} \right]$
${\rm Imp}(x, y)$ 「$(e_1) \Rightarrow (e_2)$、つまり、
$(\neg(e_1)) \lor (e_2)$のゲーデル数」
$:\equ$ ${\rm Dis}\parenth{ {\rm Neg}(x), y }$
${\rm Con}(x, y)$ 「$(e_1) \land (e_2)$、つまり、
$\neg \parenth{ (\neg(e_1)) \lor (\neg(e_2)) }$のゲーデル数」
$:\equ$ ${\rm Neg}\parenth{ {\rm Dis}\parenth{ {\rm Neg}(x), {\rm Neg}(y) } }$
${\rm Eq}(x, y)$ 「$(e_1) \Leftrightarrow (e_2)$、つまり、
$( (e_1) \Rightarrow (e_2) ) \land ( (e_2) \Rightarrow (e1) )$のゲーデル数」
$:\equ$ ${\rm Con}\parenth{ {\rm Imp}(x, y), {\rm Imp}(y, x) }$
${\rm Ex}(v, x)$ 「$\exi s(e_1)$、つまり、
$\neg \parenth{ \all s ( \neg (e_1) ) }$のゲーデル数」
$:\equ$ ${\rm Neg}\parenth{ {\rm Gen}\parenth{ v, {\rm Neg}(x) } }$
${\rm Eql}_n(x, y)$ $e_1, e_2$が$n$階のタイプの項で
$x \equ \godel{e_1}, y \equ \godel{e_2}$の時、
$n$階のタイプの項の意味で「$e_1 \equ e_2$、つまり、
$\all x_{n+1} \parenth{ x_{n+1}(e_1) \Rightarrow x_{n+1}(e_2) }$のゲーデル数」
$:\equ$ ${\rm Gen}\left[\begin{array}{@{}l@{}} 17^{n+1}, \\ {\rm Imp}\parenth{ {\rm Seq}^1(17^{n+1}) \ast {\rm Par}(x), {\rm Seq}^1(17^{n+1}) \ast {\rm Par}(y) } \end{array}\right]$ $\godel{x_{n+1}} \equ 17^{n+1}$

${\rm Z}{\text -}{\rm Ax}(x)$ 「$x$は自然数の公理のいずれかのゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & x \equ {\rm Neg}\bracket{ {\rm Eql}_1\parenth{ {\rm Seq}^2(17^1, 3), {\rm Seq}^1(1) } } \\ \lor & x \equ {\rm Imp}\left[\begin{array}{@{}l@{}} {\rm Eql}_1\parenth{ {\rm Seq}^2(17^1, 3), {\rm Seq}^2(19^1, 3) }, \\ {\rm Eql}_1\parenth{ {\rm Seq}^1(17^1), {\rm Seq}^1(19^1) } \end{array}\right] \\ \lor & x \equ {\rm Imp}\left[\begin{array}{@{}l@{}} {\rm Con}\left[\begin{array}{@{}l@{}} {\rm Seq}^4(17^2, 11, 1, 13), \\ {\rm Gen}\left[\begin{array}{@{}l@{}} 17^1, \\ {\rm Imp}\left[\begin{array}{@{}l@{}} {\rm Seq}^4(17^2, 11, 17^1, 13), \\ {\rm Seq}^5(17^2, 11, 17^1, 3, 13) \end{array}\right] \end{array}\right] \end{array}\right], \\ {\rm Gen}\left[\begin{array}{@{}l@{}} 17^1, \\ {\rm Seq}^4(17^2, 11, 17^1, 13) \end{array}\right] \end{array}\right] \end{array}\right.$
${\rm A}_1{\text -}{\rm Ax}(x)$ 「$x$は命題論理の公理(1)のゲーデル数である」 $:\Leftrightarrow$ $\exi y_{y \lt x} \parenth{ {\rm Form}(y) \land x \equ {\rm Imp}\left( {\rm Dis}(y, y), y \right) }$
${\rm A}_2{\text -}{\rm Ax}(x)$ 「$x$は命題論理の公理(2)のゲーデル数である」 $:\Leftrightarrow$ $\exi y_{y \lt x} \exi z_{z \lt x} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Form}(y) \land {\rm Form}(z) \\ \land & x \equ {\rm Imp}\left( y, {\rm Dis}(y, z) \right) \end{array}\right.$
${\rm A}_3{\text -}{\rm Ax}(x)$ 「$x$は命題論理の公理(3)のゲーデル数である」 $:\Leftrightarrow$ $\exi y_{y \lt x} \exi z_{z \lt x} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Form}(y) \land {\rm Form}(z) \\ \land & x \equ {\rm Imp}\left( {\rm Dis}(y, z), {\rm Dis}(z, y) \right) \end{array}\right.$
${\rm A}_4{\text -}{\rm Ax}(x)$ 「$x$は命題論理の公理(4)のゲーデル数である」 $:\Leftrightarrow$ $\exi y_{y \lt x} \exi z_{z \lt x} \exi w_{w \lt x} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Form}(y) \land {\rm Form}(z) \land {\rm Form}(w) \\ \land & x \equ {\rm Imp}\bracket{\begin{array}{@{}l@{}} {\rm Imp}(y, z), \\ {\rm Imp}\left( {\rm Dis}(w, y), {\rm Dis}(w, z) \right) \end{array}} \end{array}\right.$
${\rm A}{\text -}{\rm Ax}(x)$ 「$x$は命題論理の公理のゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & {\rm A}_1{\text -}{\rm Ax}(x) \\ \lor & {\rm A}_2{\text -}{\rm Ax}(x) \\ \lor & {\rm A}_3{\text -}{\rm Ax}(x) \\ \lor & {\rm A}_4{\text -}{\rm Ax}(x) \end{array}\right.$
${\rm Q}(z, y, v)$ $t$は項、$e$は論理式、$s$は変数記号で、
$z \equ \godel{t}, y \equ \godel{e}, v \equ \godel{s}$の時、
「論理式$e$の自由変数$s$に項$t$は代入可能」
$:\Leftrightarrow$ $\neg \exi n_{n \lt {\rm lh}(y)} \exi m_{m \lt {\rm lh}(z)} \exi w_{w \lt z} \left\{\begin{array}{@{}c@{}l@{}} & w \equ (z)_m \\ \land & {\rm B}(w, n, y) \land {\rm Fr}(v, n, y) \end{array}\right.$ 論理式$e$の第$n$文字目は、自由変数$s$だが、
同時に、項$t$に含まれる変数記号$s_0$でも束縛されている…
ということはない。つまり、
どの自由変数$s$に項$t$を代入しても束縛変数の個数が増えることは無い。
${\rm L}_1{\text -}{\rm Ax}(x)$ 「$x$は述語論理の公理(1)のゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}l@{}} \exi v_{v \lt x} \exi y_{y \lt x} \exi z_{z \lt x} \exi n_{n \lt x} \\ \quad\left[\begin{array}{@{}c@{}l@{}} & {\rm Var}(n, v) \land {\rm Typ}(n, z) \land {\rm Form}(y) \land {\rm Q}(z, y, v) \\ \land & x \equ {\rm Imp}\bracket{ {\rm Gen}(v, y), {\rm Sb}\!\left( y \; \displaystyle{v \atop z} \right) } \end{array}\right] \end{array}\right.$
${\rm L}_2{\text -}{\rm Ax}(x)$ 「$x$は述語論理の公理(2)のゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}l@{}} \exi v_{v \lt x} \exi p_{p \lt x} \exi q_{q \lt x} \\ \quad\left[\begin{array}{@{}c@{}l@{}} & {\rm Var}(v) \land {\rm Form}(p) \land \neg {\rm Fr}(v, p) \land {\rm Form}(q) \\ \land & x \equ {\rm Imp}\bracket{ \begin{array}{@{}l@{}} {\rm Gen}\parenth{v, {\rm Dis}(p, q)}, \\ {\rm Dis}\parenth{p, {\rm Gen}(v, q)} \end{array} } \end{array}\right] \end{array}\right.$
${\rm R}{\text -}{\rm Ax}(x)$ 「$x$は内包の公理のゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}l@{}} \exi u_{u \lt x} \exi v_{v \lt x} \exi y_{y \lt x} \exi n_{n \lt x} \\ \quad\left[\begin{array}{@{}c@{}l@{}} & {\rm Var}(n, v) \land {\rm Var}(n+1, u) \land \neg {\rm Fr}(u, y) \land {\rm Form}(y) \\ \land & x \equ {\rm Ex}\bracket{u, {\rm Gen}\bracket{v, {\rm Eq}\bracket{ \begin{array}{@{}l@{}} {\rm Seq}^1(u) \ast {\rm Par}\parenth{ {\rm Seq}^1(v) }, \\ y \end{array} } } } \end{array}\right] \end{array}\right.$
${\rm Ext}_1$ 「$n \equ 1$の時の外延性の公理のゲーデル数」 $:\Leftrightarrow$ ${\rm Imp}\bracket{\begin{array}{@{}l@{}} {\rm Gen}\bracket{ 17^1, {\rm Eq}\bracket{\begin{array}{@{}l@{}} {\rm Seq}^4(17^2, 11, 17^1, 13), \\ {\rm Seq}^4(19^2, 11, 17^1, 13) \end{array} } }, \\ {\rm Eql}_2(17^2, 19^2) \end{array}}$
${\rm E}{\text -}{\rm Ax}(x)$ 「$x$は外延性の公理のゲーデル数である」 $:\Leftrightarrow$ $\exi n_{n \lt x} \bracket{ x \equ {\rm Te}(n, {\rm Ext}_1) }$
${\rm Ax}(x)$ 「$x$はいづれかの公理のゲーデル数である」 $:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & {\rm Z}{\text -}{\rm Ax}(x) \\ \lor & {\rm A}{\text -}{\rm Ax}(x) \\ \lor & {\rm L}_1{\text -}{\rm Ax}(x) \lor {\rm L}_2{\text -}{\rm Ax}(x) \\ \lor & {\rm R}{\text -}{\rm Ax}(x) \\ \lor & {\rm E}{\text -}{\rm Ax}(x) \end{array}\right.$
${\rm Ic}(x)$ ${\mathbf A}_1, {\mathbf A}_2, {\mathbf A}_3$は論理式で
$x \equ \godel{{\mathbf A}_1}, y \equ \godel{{\mathbf A}_2}, z \equ \godel{{\mathbf A}_3}$の時、
「$x$は、${\mathbf A}_2$と${\mathbf A}_3$、あるいは、
${\mathbf A}_2$から得られる結果の論理式のゲーデル数である。」
$:\Leftrightarrow$ $\left\{\begin{array}{@{}c@{}l@{}} & z \equ {\rm Imp}(y, x) \\ \lor & \exi v_{v \lt x}\bracket{ {\rm Var}(v) \land x \equ {\rm Gen}(v, y) } \end{array}\right.$
${\rm Pf}(x)$ 「$x$は証明図のゲーデル数である」 $:\Leftrightarrow$ $\all n_{n \lt {\rm lh}(x)} \left\{\begin{array}{@{}c@{}l@{}} & {\rm Ax}((x)_n) \\ \lor & \exi p_{p \lt n} \exi q_{q \lt n} \; {\rm Ic}((x)_n, (x)_p, (x)_q) \end{array}\right.$
${\rm P}(x, y)$ $e$は表現、${\mathbf A}$は論理式で
$x \equ \godel{e}, y \equ \godel{{\mathbf A}}$の時、
「$e$は${\mathbf A}$の証明図である」
$:\Leftrightarrow$ ${\rm Pf}(x) \land (x)_{{\rm lh}(x) \dot{-} 1} \equ y$

${\rm Prov}(x)$ 「$x$は証明可能な論理式のゲーデル数である」 $:\Leftrightarrow$ $\exi y \parenth{ {\rm P}(y, x) }$
${\rm Prov}(x)$は原始帰納的述語ではない。帰納的述語でさえもない。束縛変数$y$が有界でないことに注意。