形式的体系${\cal R}$を定義する
今週のお題「最近おいしかったもの」}
形式的体系${\cal R}$を定義する。 (参考文献:廣瀬健、「帰納的関数」、75ページ~81ページ)- ${\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$等の文字を用いる事がある。
- 定記号:
- ${\cal R}$における項(term)
- 対象記号${\mathbf 0}$は項である。
- 変数記号$a_i$は項である$\left(i \equ 0, 1, 2, \cdots\right)$。
- $t$が項であるとき、$(t)^\prime$は項である。
- $f$が関数記号で、$t_1,t_2,\cdots,t_n$がいづれも項のとき、$f(t_1,t_2,\cdots,t_2)$は項である。
- 以上によって定義されるもののみが項である。
- 補助記号$(,)$を用いなくても項の構成の順序が明瞭な場合には適当に省略する。
- ${\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$と書く事にする。
- 方程式(equation)
$t_1,t_2$が項の時、$t_1 \equ t_2$を方程式という。$t_1$をこの方程式の左辺、$t_2$をこの方程式の右辺という。 - 方程式系(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$の左辺の一番左が必ず関数記号であるものと約束する。 - 推論規則(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)$
以下、この推論規則を"代入(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)$
以下、この推論規則を"置換(replacement)"と呼ぶ。
- $e$を方程式、$a$を$e$に含まれる変数、$n$を数項とする。
- 演繹(deduction)
方程式のある集合を$E$とする(有限とは限らない)。ここで定義されるものは、正確には、「$E$からの演繹(deduction from $E$)」である。
- $e$を$E$に含まれる方程式とするとき、
$e$は、$E$からの演繹である。 この時、$e$はこの演繹の最下式であるという。
- $D$を$E$からの演繹とし、$D$の最下式を$e_1$とするとき、$e_1$から"代入"の推論規則によって$e_2$が得られるならば、
$D$ $e_2$ - $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$を$E$に含まれる方程式とするとき、
- 関数表(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$に対応する数項である。 - 主関数記号(principal function letter)
$E$を方程式系$(e_0,e_1,\cdots,e_l)$とする。
$e_l$の左辺の一番左の記号(約束によって、関数記号)を、主関数記号という。
$E$の中で、方程式の右辺には現れるが左辺に現れない関数記号を、(関数表で)与えられた関数記号(given function letter)と呼ぶ。
$E$の中で、方程式の右辺にも左辺にも現れる、主関数記号以外の関数記号を、補助関数記号(auxiliary function letter)と呼ぶ。 - 演繹可能な方程式
$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}$と書くわけである。
- 部分関数$\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$が満たす条件の内、$\Rightarrow$が成り立つ事を、$E$の無矛盾性と呼び、$\Leftarrow$が成り立つ事を、$E$の完全性という。