帰納的関数論 1
形式的体系とは、(形式主義の立場では)有限の立場とよばれる構成的な方法で証明論を形式化し、さらに証明論の対象である個々の数学的理論をも、同じように形式化したものである。従って、形式的体系における思考対象を定義する方法、論理の運用は有限の立場においてなされる。つまり、形式的体系における議論の展開は有限の立場によって行われる。
原始帰納的という概念こそが、形式的体系での有限の立場の自然数論における像であり、その概念自身、有限の立場によるものなのである。
有限の立場とは、大雑把に言えば、有限回の操作によって実行可能な事柄のみを、そのよりどころとする立場である。すなわち、構成の概念がその中心である。
有限の立場での議論の対象は、目前にある有限個の記号、およびその有限個の組合せである。これをいま、図形と呼ぼう。
次のような無限の図形を定義する方法を、帰納的定義と呼ぶ：
- 具体的な記号を定める。これは1つの図形である。
- 具体的な図形がいくつか与えられた時、これから具体的な(新しい)図形を作り出す手段を定める。
- 以上によって定められる物のみが図形である。それ以外は(現在定義しようとしている)図形では無い。
次のようにして、有限の立場における自然数が定義される：
- $0$は自然数である。
- $n$が自然数ならば、$n^\prime$は自然数である。
- 以上によって定められる物のみが自然数である。
このように定義すれば、自然数とは、$0, 0^\prime, 0^{\prime \prime}, 0^{\prime \prime \prime}, \cdots$のような図形を意味するわけである(もちろん、$0^\prime$を$1$と書き、$0^{\prime\prime}$を$2$と書き、…と約束して、以下そのように書いてもよい。しかし、構成された図形としての自然数はあくまで、$0, 0^\prime, 0^{\prime\prime}, \cdots$の形をしている)。
一般に、$\varphi_i(a_1, \cdots, a_m) (i \equ 1, 2, \cdots, k)$ を $a_1, \cdots, a_m$ から、何らかの定まった操作で得られる物として、次のようなAの帰納的定義を考える：
- $\alpha_1, \cdots, \alpha_n$ は $A$ である。
- $a_1, \cdots, a_m$ が $A$ である時、$\varphi_1(a_1, \cdots, a_m), \cdots, \varphi_k(a_1, \cdots, a_m)$ は $A$ である。
- 以上によるもののみが $A$ である。
この時、任意の $A$ であるような $x$ について、ある性質 $P(x)$ を証明したいとしよう。このためには、$A$ の帰納的定義に従って、次のような帰納法を用いればよい：
- $P(\alpha_1), \cdots, P(\alpha_n)$ が成り立つことを示す。
- $A$であるような任意の$a_1, \cdots, a_m$ について、$P(a_1), \cdots, P(a_m)$であることを仮定して、$P(\varphi_1(a_1, \cdots, a_m)), \cdots, P(\varphi_k(a_1, \cdots, a_m))$ が成り立つことを示す。
記号と規約
$X \subseteq {\mathbb N}^n$とする。
$\varphi, \psi$を$\mathbb{N}^n$上の部分関数とする。
部分述語$\varphi \equ \psi$を以下で定義する：
$\mathbb{N}^n$上全域で定義された述語$\varphi \simeq \psi$を以下で定義する：
関数$\varphi : X \rightarrow {\mathbb N}$を${\mathbb N}^n$上の部分関数とも言う。
$P$は$X$上で定義されている述語とする。$\chi_P : X \rightarrow {\mathbb N}, (x_1, \cdots, x_n) \mapsto \left\{\begin{array}{@{}@{}@{}} 0 & ( P(x_1, \cdots, x_n) ) \\ 1 & ( \neg P(x_1, \cdots, x_n) ) \end{array}\right.$
で定義される関数を$P$の表現関数(representing function)という。
述語$P$は$\mathbb{N}^n$上の部分述語である。 $:\Leftrightarrow$ 述語$P$の表現関数$\chi_P$は$\mathbb{N}^n$上の部分関数である。
$\varphi, \psi$を$\mathbb{N}^n$上の部分関数とする。
部分述語$\varphi \equ \psi$を以下で定義する：
| $\varphi(x_1, \cdots, x_n)$ | $\psi(x_1, \cdots, x_n)$ | $\varphi(x_1, \cdots, x_n) \equ \psi(x_1, \cdots, x_n)$の真理値 |
|---|---|---|
| 定義されている | 定義されている | 関数値$\varphi(x_1, \cdots, x_n)$と$\psi(x_1, \cdots, x_n)$の値が等しければ真 |
| 関数値$\varphi(x_1, \cdots, x_n)$と$\psi(x_1, \cdots, x_n)$の値が等しくなければ偽 | ||
| それ以外 | 定義されていない | |
| $\varphi(x_1, \cdots, x_n)$ | $\psi(x_1, \cdots, x_n)$ | $\varphi(x_1, \cdots, x_n) \simeq \psi(x_1, \cdots, x_n)$の真理値 |
|---|---|---|
| 定義されている | 定義されている | 関数値$\varphi(x_1, \cdots, x_n)$と$\psi(x_1, \cdots, x_n)$の値が等しければ真 |
| 関数値$\varphi(x_1, \cdots, x_n)$と$\psi(x_1, \cdots, x_n)$の値が等しくなければ偽 | ||
| 定義されている | 定義されていない | 偽 |
| 定義されていない | 定義されている | 偽 |
| 定義されていない | 定義されていない | 真 |
以下では、特に部分関数、部分述語と断らない限り、全域で定義されているとする。
原始帰納的関数と帰納的関数
原始帰納的関数(述語)は、形式的体系における有限の立場での手続き、ないしは、この立場で定義された論理式の自然数論における解釈としての表現をその起源とする。
帰納的関数(述語)は、アルゴリズムを持つ関数(述語)の数学的定義として適当と考えられる概念である。
以下で取り扱われる関数は、自然数上で定義され、自然数値をとる数論的関数であり、述語もまた自然数上で定義されるもののみを考える。
帰納的関数を定義する図式(schema)
(${\cal D}$-)(原始)帰納的記述
$\varphi_1, \cdots, \varphi_l, \varphi$は関数とする。${\cal D}$は関数の有限集合とする。
(${\cal D}$-)(原始)帰納的関数
$\varphi$は関数とする。${\cal D}$は関数の有限集合とする。
- 初期関数(initial function)
- 後者関数(successor function):
$\varphi(x) \equ x^\prime$
- 定数関数:($q$は定数)
$\varphi(x_1, \cdots, x_n) \equ q$
- 射影関数:($n \equ 1$なら恒等関数)
$\varphi(x_1, \cdots, x_n) \equ x_i \parenth{ i \equ 1, \cdots, n }$
- 後者関数(successor function):
- 与えられた関数から得られる関数(immediate consequence)
- 合成:
$\psi$は$m$変数関数、$\chi_1, \cdots, \chi_m$は$n$変数関数とする。$\varphi(x_1, \cdots, x_n) \equ \psi(\chi_1(x_1, \cdots, x_n), \cdots, \chi_m(x_1, \cdots, x_n))$ - 帰納的定義:
$\psi$は$n$変数関数、$\chi$は$n+2$変数関数とする。$\left\{\begin{array}{} \varphi(0, x_1, \cdots, x_n) & \equ & \psi(x_1, \cdots, x_n) \\ \varphi(x^\prime, x_1, \cdots, x_n) & \equ & \chi(x, \varphi(x, x_1, \cdots, x_n), x_1, \cdots, x_n) \\ \end{array}\right.$ - $\mu$-作用素の適用もしくは最小化の操作:
$\psi$は$n+1$変数関数とする。
$\all x_1 \cdots \all x_n \exi y \; \parenth{ \psi(x_1, \cdots, x_n, y) \equ 0 }$が成立していると仮定する。$\varphi(x_1, \cdots, x_n) \equ \mu y \parenth{ \psi(x_1, \cdots, x_n, y) \equ 0 }$ただし、$\mu y \parenth{ \psi(x_1, \cdots, x_n, y) \equ 0 }$は、$x_1, \cdots, x_n$に対し、$\psi(x_1, \cdots, x_n, y) \equ 0$を満たす最小の$y$を表す。仮定により、このような値が存在する。
- 合成:
(${\cal D}$-)(原始)帰納的記述
$\varphi_1, \cdots, \varphi_l, \varphi$は関数とする。${\cal D}$は関数の有限集合とする。
| $\varphi_1, \cdots, \varphi_l$は$\left\{\begin{array}{@{}@{}@{}} \varphi{\rm についての}{\cal D}{\rm -帰納的記述} {\rm 、あるいは、} \\ {\cal D}{\rm からの帰納的記述} \end{array}\right.$ | $:\Leftrightarrow$ |
| $\left\{\begin{array}{@{}@{}@{}} \left.\begin{array}{@{}@{}} {\rm 任意の}i \equ 1, \cdots, l{\rm について、} \\ \quad\left\{\begin{array}{@{}@{}@{}@{}} (1) & \varphi_i {\rm は初期関数} & {\rm または} \\ (2) & \varphi_i {\rm は}{\cal D}{\rm の要素} & {\rm または} \\ (3) & \begin{array}{} j_1, \cdots, j_m \lt i {\rm が存在して} \\ \quad \varphi_i {\rm は関数} \varphi_{j_1}, \cdots, \varphi_{j_m} {\rm から得られる関数} \end{array} \end{array}\right. \end{array}\right) & {\rm かつ} \\ \psi_l \equ \varphi & \end{array}\right.$ | |
${\cal D} \equ \phi$の時は、$\varphi_1, \cdots, \varphi_l$を帰納的記述という。
| $\varphi_1, \cdots, \varphi_l$は$\left\{\begin{array}{@{}@{}@{}} \varphi{\rm についての}{\cal D}{\rm -原始帰納的記述} {\rm 、あるいは、} \\ {\cal D}{\rm からの原始帰納的記述} \end{array}\right.$ | $:\Leftrightarrow$ |
| $\left\{\begin{array}{@{}@{}@{}} \left.\begin{array}{@{}@{}} {\rm 任意の}i \equ 1, \cdots, l{\rm について、} \\ \quad\left\{\begin{array}{@{}@{}@{}@{}} (1) & \varphi_i {\rm は初期関数} & {\rm または} \\ (2) & \varphi_i {\rm は}{\cal D}{\rm の要素} & {\rm または} \\ (3) & \begin{array}{} j_1, \cdots, j_m \lt i {\rm が存在して} \\ \quad \begin{array}{@{}@{}} \varphi_i {\rm は関数} \varphi_{j_1}, \cdots, \varphi_{j_m} {\rm から} \\ {\rm 合成、帰納的定義の操作によって得られる関数} \end{array} \end{array} \end{array}\right. \end{array}\right) & {\rm かつ} \\ \psi_l \equ \varphi & \end{array}\right.$ | |
${\cal D} \equ \phi$の時は、$\varphi_1, \cdots, \varphi_l$を原始帰納的記述という。
(${\cal D}$-)(原始)帰納的関数
$\varphi$は関数とする。${\cal D}$は関数の有限集合とする。
| $\varphi$は${\cal D}$-帰納的関数 | $:\Leftrightarrow$ | $\begin{array}{@{}@{}} {\rm 関数}\varphi_1, \cdots, \varphi_l{\rm が存在して、} \\ \quad \varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての}{\cal D}-{\rm 帰納的記述} \end{array}$ |
${\cal D} \equ \phi$の時は、$\varphi$を帰納的関数という。
| $\varphi$は${\cal D}$-原始帰納的関数 | $:\Leftrightarrow$ | $\begin{array}{@{}@{}} {\rm 関数}\varphi_1, \cdots, \varphi_l{\rm が存在して、} \\ \quad \varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての}{\cal D}-{\rm 原始帰納的記述} \end{array}$ |
${\cal D} \equ \phi$の時は、$\varphi$を原始帰納的関数という。
定理
$\varphi$は関数とする。${\cal D}$は関数の有限集合とする。
- $\varphi$は${\cal D}$-原始帰納的関数 $\Rightarrow$ $\varphi$は${\cal D}$-帰納的関数 が成り立つ。
- $\left\{\begin{array}{@{}@{}@{}} \varphi {\rm は}{\cal D}-原始帰納的関数 & {\rm かつ} \\ {\rm 任意の}\varphi_0 \in {\cal D}に対し、\varphi_0 {\rm は原始帰納的関数} & \end{array}\right. \Rightarrow \varphi {\rm は原始帰納的関数}$ が成り立つ。
- $\left\{\begin{array}{@{}@{}@{}} \varphi {\rm は}{\cal D}-帰納的関数 & {\rm かつ} \\ {\rm 任意の}\varphi_0 \in {\cal D}に対し、\varphi_0 {\rm は帰納的関数} & \end{array}\right. \Rightarrow \varphi {\rm は帰納的関数}$ が成り立つ。
原始帰納的関数の例を複数挙げる。
$\left\{\begin{array}{@{}@{}@{}@{}} 0 + b & \equ & b, \\ a^\prime + b & \equ & ( a + b )^\prime \end{array}\right.$で定義された和$a+b$は原始帰納的関数である。
- $\varphi_1(x) \equ x^\prime, \varphi_2(b) \equ b, \varphi_3(a, x, b) \equ x, \varphi_4(a, x, b) \equ \varphi_1(\varphi_3(a, x, b)), $
$\left\{\begin{array}{@{}@{}@{}@{}} \varphi_5(0, b) & \equ & \varphi_2(b), \\ \varphi_5(a^\prime, b) & \equ & \varphi_4(a, \varphi_5(a, b), b) \end{array}\right.$と置く。 - $\varphi_1, \cdots, \varphi_5 {\rm は}a+b{\rm についての原始帰納的記述}$である。
一般に、関数$f$が原始帰納的関数であることを示す時、原始帰納的記述を作るのは煩雑である。
上のように定義式を書いただけでも、その原始帰納的記述をうかがい知ることは十分出来るから、以後は殆ど上のように簡略化する。
- $\varphi_1(x) \equ x^\prime, \varphi_2(b) \equ b, \varphi_3(a, x, b) \equ x, \varphi_4(a, x, b) \equ \varphi_1(\varphi_3(a, x, b)), $
- $\left\{\begin{array}{@{}@{}@{}@{}} 0 \cdot b & \equ & 0, \\ a^\prime \cdot b & \equ & a \cdot b + b \end{array}\right.$
- $\left\{\begin{array}{@{}@{}@{}@{}} a^0 & \equ & 1, \\ a^{b^\prime} & \equ & a^b \cdot a \end{array}\right.$
- $\left\{\begin{array}{@{}@{}@{}@{}} 0! & \equ & 1, \\ a^\prime! & \equ & a! \cdot a^\prime \end{array}\right.$
- "$a$の前者(predecessor)をとる"関数
$\left\{\begin{array}{@{}@{}@{}@{}} pd(0) & \equ & 0, \\ pd(a^\prime) & \equ & a \end{array}\right.$ - $a \dot{-} b \equ \left\{\begin{array}{@{}@{}@{}@{}} a - b & \parenth{ a \geq b {\rm の時} } \\ 0 & \parenth{ a \lt b {\rm の時} } \end{array}\right.$なる関数
$\left\{\begin{array}{@{}@{}@{}@{}} a \dot{-} 0 & \equ & a, \\ a \dot{-} b^\prime & \equ & pd(a \dot{-} b) \end{array}\right.$ - "$a, b$の小さい方をとる"関数
$\min(a, b) \equ b \dot{-} ( b \dot{-} a )$ - "$a_1, a_2, \cdots, a_n$のうち、一番小さいものをとる"関数
$\min(a_1, a_2, \cdots, a_n) \equ \min( \cdots \min(\min(a_1, a_2), a_3), \cdots, a_n)$ - "$a, b$の大きい方をとる"関数
$\max(a, b) \equ (a+b) \dot{-} \min(a, b)$ - "$a_1, a_2, \cdots, a_n$のうち、一番大きいものをとる"関数
$\max(a_1, a_2, \cdots, a_n) \equ \max( \cdots \max(\max(a_1, a_2), a_3), \cdots, a_n)$ - $\left\{\begin{array}{@{}@{}@{}@{}} {\rm sg}(0) & \equ & 0, \\ {\rm sg}(a^\prime) & \equ & 1 \end{array}\right.$
- $\left\{\begin{array}{@{}@{}@{}@{}} \overline{\rm sg}(0) & \equ & 1, \\ \overline{\rm sg}(a^\prime) & \equ & 0 \end{array}\right.$
- $|a - b| \equ (a \dot{-} b) + (b \dot{-} a)$
- "$a$を$b$で割った剰余をとる"関数、つまり、
${\rm rem}(a, b) \equ \left\{\begin{array}{@{}@{}@{}@{}} a & & (b \equ 0 {\rm の時}) \\ (a \equ b \cdot q + r, 0 \leq r \lt b {\rm であるような}r) & & (b \neq 0 {\rm の時}) \end{array}\right.$なる関数。 $\left\{\begin{array}{@{}@{}@{}@{}} {\rm rem}(0, b) & \equ & 0 \\ {\rm rem}(a^\prime, b) & \equ & ({\rm rem}(a, b) + 1) \cdot {\rm sg}(|b - ({\rm rem}(a, b) + 1)|) \end{array}\right.$ - $\bracket{ \dfrac{a}{b} } \equ \left\{\begin{array}{@{}@{}@{}@{}} 0 & (b \equ 0 {\rm の時}) \\ (a {\rm を}b{\rm で割った商の整数部分}) & (b \neq 0 {\rm の時}) \end{array}\right.$なる関数。
$\left\{\begin{array}{@{}@{}@{}@{}} \bracket{ \dfrac{0}{b} } & \equ & b \\ \bracket{ \dfrac{a^\prime}{b} } & \equ & \bracket{ \dfrac{a}{b} } + \overline{\rm sg}(|b - ({\rm rem}(a, b) + 1)|) \end{array}\right.$ - 対関数(pairing function)と呼ばれる可逆写像:${\mathbb N} \times {\mathbb N} \rightarrow {\mathbb N}$
$j(a, b) \equ \bracket{ \dfrac{ (a+b)(a+b+1) }{ 2 } } + a$
$\psi$を関数とする。$\psi$-原始帰納的関数を定義する。
- $\left\{\begin{array}{@{}c@{}l@{}c@{}l@{}} {\displaystyle \sum\limits_{y \lt 0}} & \psi(x_1, \cdots, x_n, y) & \equ & 0, \\ {\displaystyle \sum\limits_{y \lt z+1}} & \psi(x_1, \cdots, x_n, y) & \equ & \psi(x_1, \cdots, x_n, z) + {\displaystyle \sum\limits_{y \lt z}} \psi(x_1, \cdots, x_n, y) \end{array}\right.$
- $\begin{array}{@{}c@{}l@{}c@{}c@{}l@{}} {\displaystyle \sum\limits_{y \leq z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \sum\limits_{y \lt z+1}} & \psi(x_1, \cdots, x_n, y) \\ {\displaystyle \sum\limits_{w \lt y \lt z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \sum\limits_{y \lt z \dot{-} (w+1)}} & \psi(x_1, \cdots, x_n, y+w+1) \\ {\displaystyle \sum\limits_{w \leq y \leq z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \sum\limits_{y \lt (z \dot{-} w)+1}} & \psi(x_1, \cdots, x_n, y+w) \end{array}$
- $\left\{\begin{array}{@{}c@{}l@{}c@{}l@{}} {\displaystyle\prod\limits_{y \lt 0}} & \psi(x_1, \cdots, x_n, y) & \equ & 1, \\ {\displaystyle\prod\limits_{y \lt z+1}} & \psi(x_1, \cdots, x_n, y) & \equ & \psi(x_1, \cdots, x_n, z) \cdot {\displaystyle\prod\limits_{y \lt z}} \psi(x_1, \cdots, x_n, y) \end{array}\right.$
- $\begin{array}{@{}c@{}l@{}c@{}c@{}l@{}} {\displaystyle \prod\limits_{y \leq z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \prod\limits_{y \lt z+1}} & \psi(x_1, \cdots, x_n, y) \\ {\displaystyle \prod\limits_{w \lt y \lt z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \prod\limits_{y \lt z \dot{-} (w+1)}} & \psi(x_1, \cdots, x_n, y+w+1) \\ {\displaystyle \prod\limits_{w \leq y \leq z}} & \psi(x_1, \cdots, x_n, y) & \equ & {\displaystyle \prod\limits_{y \lt (z \dot{-} w)+1}} & \psi(x_1, \cdots, x_n, y+w) \end{array}$
