$ \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}$を定義する。 (参考文献:廣瀬健、「帰納的関数」、75ページ~81ページ)
  1. ${\cal R}$の基本記号
    • 定記号:
      • 対象記号として、${\mathbf 0}$
      • (特定の)関数記号として、$^\prime$
      • 述語記号として、$\equ$
      • 補助記号として、$($、$)$、$,$
    • 変数および関数記号:
      • 変数を表す記号として、$a,a_|,a_{||},a_{|||},a_{||||},\cdots$
      • 関数を表す記号として、$f,f_|,f_{||},f_{|||},f_{||||},\cdots$
      • 以後、
        $a,a_|,a_{||},a_{|||},a_{||||},\cdots$をそれぞれ
        $a,a_1,a_{2},a_{3},a_{4},\cdots$と書き、
        $f,f_|,f_{||},f_{|||},f_{||||},\cdots$をそれぞれ
        $f,f_1,f_{2},f_{3},f_{4},\cdots$と書く事にする。
      • $^\prime$も関数記号なのであるが、これは、予め定められた特殊な関数記号であるから、 単に関数記号という場合は、このリストの内の1つを指すものとする。
      • 以後、見やすくするために、 変数記号として、$x,y,z,\cdots$、関数記号として、$g,h,\cdots$等の文字を用いる事がある。
  2. ${\cal R}$における項(term)
    1. 対象記号${\mathbf 0}$は項である。
    2. 変数記号$a_i$は項である$\left(i \equ 0, 1, 2, \cdots\right)$。
    3. $t$が項であるとき、$(t)^\prime$は項である。
    4. $f$が関数記号で、$t_1,t_2,\cdots,t_n$がいづれも項のとき、$f(t_1,t_2,\cdots,t_2)$は項である。
    5. 以上によって定義されるもののみが項である。
    6. 補助記号$(,)$を用いなくても項の構成の順序が明瞭な場合には適当に省略する。
    7. ${\mathbf 0}, {\mathbf 0}^\prime, {\mathbf 0}^{\prime\prime}, {\mathbf 0}^{\prime\prime\prime}, \cdots$ を数項(numeral)と呼ぶ。以後、これをそれぞれ、
      $0,1,2,3,\cdots$、あるいは、$\bar{0},\bar{1},\bar{2},\bar{3},\cdots$と書く事にする。
  3. 方程式(equation)
    $t_1,t_2$が項の時、
    $t_1 \equ t_2$
    を方程式という。$t_1$をこの方程式の左辺、$t_2$をこの方程式の右辺という。
  4. 方程式系(system of equations)
    方程式$e_0,e_1,\cdots,e_l$による有限列$(e_0,e_1,\cdots,e_l)$を方程式系という。
    以後、記述を簡単にするため、方程式系$(e_0,e_1,\cdots,e_l)$とは、$e_l$の左辺の一番左が必ず関数記号であるものと約束する。
  5. 推論規則(rules of inference)
    $e$を方程式、$a$を変数、$n$を数項とする。
    $e$の中に変数$a$が現れていれば、その全ての$a$を$n$で置き換えて得られる方程式を、
    ${\rm Sub}(e; a, n)$
    と書き表す。
    $t$を項、$f$を関数記号とし、$n_1,n_2,\cdots,n_r, n$を数項とする。
    $t$の中に$f(n_1,n_2,\cdots,n_r)$が含まれていれば、その全てを$n$で置き換えて得られる項を、
    ${\rm Rep}(t; f(n_1,n_2,\cdots,n_r),n)$
    と書き表す。
    • $e$を方程式、$a$を$e$に含まれる変数、$n$を数項とする。
      $e$

      ${\rm Sub}(e; a, n)$
      は推論規則である。このとき、「$e$から推論規則によって${\rm Sub}(e; a, n)$が得られる」という。
      以下、この推論規則を"代入(substitution)"と呼ぶ。
    • $n_1,n_2,\cdots,n_r,n$を数項、$f$を関数記号とし、 $s \equ t$は変数を含まない方程式で、右辺$t$が$f(n_1,n_2,\cdots,n_r)$を含むものとする。
      $s \equ t$ $f(n_1,n_2,\cdots,n_r) \equ n$

      $s \equ {\rm Rep}(t; f(n_1,n_2,\cdots,n_r),n)$
      は推論規則である。 このとき、「$s \equ t$と$f(n_1,n_2,\cdots,n_r) \equ n$から、推論規則によって$s \equ {\rm Rep}(t; f(n_1,n_2,\cdots,n_r),n)$が得られる」という。
      以下、この推論規則を"置換(replacement)"と呼ぶ。
  6. 演繹(deduction)
    方程式のある集合を$E$とする(有限とは限らない)。ここで定義されるものは、正確には、「$E$からの演繹(deduction from $E$)」である。
    1. $e$を$E$に含まれる方程式とするとき、
      $e$
      は、$E$からの演繹である。 この時、$e$はこの演繹の最下式であるという。
    2. $D$を$E$からの演繹とし、$D$の最下式を$e_1$とするとき、$e_1$から"代入"の推論規則によって$e_2$が得られるならば、
      $D$

      $e_2$
      は、$E$からの演繹である。このとき、$e_2$はこの演繹の最下式であるという。
    3. $D_1,D_2$を$E$からの演繹とし、$D_1$の最下式を$e_1$、$D_2$の最下式を$e_2$とする。 $e_1$と$e_2$から、"置換"の推論規則によって、$e_3$が得られるならば、
      $D_1$ $D_2$

      $e_3$
      は、$E$からの演繹である。このとき、$e_3$はこの演繹の最下式であるという。
    4. 以上によって定められるもののみが、$E$からの演繹である。
  7. 関数表(given functions)
    変数を含まない方程式の集合を、関数表という。
    自然数上で定義された関数$\psi_1,\cdots,\psi_m$が与えられているものとする。
    $g_1,\cdots,g_m$を$\psi_1,\cdots,\psi_m$に対応する${\cal R}$での関数記号として用いるものとする。
    $E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m} :\equiv \bigcup\limits_{i \equ 1}^m \Set{ g_i({\overline n}_1,\cdots,{\overline n}_{l_i}) \equ {\overline n} } { \psi_i(n_1,\cdots,n_{l_i}) \equ n \; ( n_1,\cdots,n_{l_i}, n は自然数 ) }$
    を$\psi_1,\cdots,\psi_m$に対する関数表と呼ぶ。
    ただし、${\overline n}_1,\cdots,{\overline n}_{l_i}, {\overline n}$は、それぞれ自然数$n_1,\cdots,n_{l_i}, n$に対応する数項である。
  8. 主関数記号(principal function letter)
    $E$を方程式系$(e_0,e_1,\cdots,e_l)$とする。
    $e_l$の左辺の一番左の記号(約束によって、関数記号)を、主関数記号という。
    $E$の中で、方程式の右辺には現れるが左辺に現れない関数記号を、(関数表で)与えられた関数記号(given function letter)と呼ぶ。
    $E$の中で、方程式の右辺にも左辺にも現れる主関数記号以外の関数記号を、補助関数記号(auxiliary function letter)と呼ぶ。
  9. 演繹可能な方程式
    $E$を方程式系、$E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}$を関数表とする。
    $E \cup E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}$からの演繹の最下式となるような方程式$f({\overline n}_1,\cdots,{\overline n}_r) \equ {\overline n}$を、 $E$と$E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}$から演繹可能(deducible from $E, E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}$)な方程式と呼び、
    $E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}, E \vdash f({\overline n}_1,\cdots,{\overline n}_r) \equ {\overline n}$
    と書く。
    $E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}$が空のときは、もちろん、単に
    $E \vdash f({\overline n}_1,\cdots,{\overline n}_r) \equ {\overline n}$
    と書くわけである。
以上によって、形式的体系${\cal R}$は定められた。
  • 部分関数$\varphi(z_1,\cdots,z_n)$が形式的に計算可能(formally calculable)であるとは、
    $\varphi$に対して、ある方程式系$E$が存在して、任意の自然数$z_1,\cdots,z_n,z$と、それに対応する数項${\overline z}_1,\cdots,{\overline z}_n,{\overline z}$について、
    $E \vdash f({\overline z}_1,\cdots,{\overline z}_n) \equ {\overline z} \Leftrightarrow \varphi(z_1,\cdots,z_n) \equ z$
    が成り立つときをいう。ただし、$f$は$E$の主関数記号とする。
  • 部分関数$\varphi(z_1,\cdots,z_n)$が関数$\varphi_1,\cdots,\varphi_m$から形式的に計算可能(formally calculable from $\varphi_1,\cdots,\varphi_m$)であるとは、
    $\varphi$に対して、ある方程式系$E$が存在して、任意の自然数$z_1,\cdots,z_n,z$と、それに対応する数項${\overline z}_1,\cdots,{\overline z}_n,{\overline z}$について、
    $E_{g_1,\cdots,g_m}^{\psi_1,\cdots,\psi_m}, E \vdash f({\overline z}_1,\cdots,{\overline z}_n) \equ {\overline z} \Leftrightarrow \varphi(z_1,\cdots,z_n) \equ z$
    が成り立つときをいう。ただし、$f$は$E$の主関数記号とする。
この定義における方程式系$E$を、「関数$\varphi$を形式的に定義する方程式系」と呼ぶ。
また、$E$が満たす条件の内、$\Rightarrow$が成り立つ事を、$E$の無矛盾性と呼び、$\Leftarrow$が成り立つ事を、$E$の完全性という。