帰納的関数論 2
$P(x_1, \cdots, x_n)$は自然数上で定義された述語とする。
${\cal D}$は関数の有限集合とする。
$\varphi$は関数とする。
${\cal Q}$は述語の有限集合とする。
${\cal D}$は関数の有限集合とする。
| $P$は${\cal D}$-帰納的述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P$は${\cal D}$-帰納的関数 |
${\cal D} \equ \phi$の時は、$P$を帰納的述語という。
| $P$は${\cal D}$-原始帰納的述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P$は${\cal D}$-原始帰納的関数 |
${\cal D} \equ \phi$の時は、$P$を原始帰納的述語という。
$\varphi$は関数とする。
${\cal Q}$は述語の有限集合とする。
| $\varphi$は${\cal Q}$-帰納的関数 | $:\Leftrightarrow$ | $\varphi$は$\Set{ {\rm 述語}Q{\rm の表現関数}\chi_Q }{ Q \in {\cal Q} }$-帰納的関数 |
| $P$は${\cal Q}$-帰納的述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P$は${\cal Q}$-帰納的関数 |
| $\varphi$は${\cal Q}$-原始帰納的関数 | $:\Leftrightarrow$ | $\varphi$は$\Set{ {\rm 述語}Q{\rm の表現関数}\chi_Q }{ Q \in {\cal Q} }$-原始帰納的関数 |
| $P$は${\cal Q}$-原始帰納的述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P$は${\cal Q}$-原始帰納的関数 |
定理
$\varphi$は関数とする。$P$は述語とする。
${\cal D}$は関数の有限集合とする。
${\cal Q}$は述語の有限集合とする。
$P(y_1, \cdots, y_m)$を述語、$(\varphi_i(x_1, \cdots, x_n))_{i=1}^m$を関数の有限列とする。
$P(\varphi_1(x_1, \cdots, x_n), \cdots, \varphi_m(x_1, \cdots, x_n)) {\rm は}\braces{ \chi_P, \varphi_1, \cdots, \varphi_m }{\text -}{\rm 原始帰納的述語}$が成り立つ。
$P(x_1, \cdots, x_n), Q(x_1, \cdots, x_n)$を述語とする。
以下に定義される関数は、$\braces{ P }{\text -}{\rm 原始帰納的関数}$である。
$(\psi_i(x_1, \cdots, x_n))_{i=1}^{m+1}$を関数の有限列とする。
$(P_i(x_1, \cdots, x_n))_{i=1}^m$を述語の有限列とし、これらのどの2つをとっても同時に成立することは無いとする。 $\varphi(x_1, \cdots, x_n) :\equiv \left\{\begin{array}{@{}@{}} \psi_1(x_1, \cdots, x_n) & (P_1(x_1, \cdots, x_n) {\rm の時}) \\ \cdots & \cdots \\ \psi_m(x_1, \cdots, x_n) & (P_m(x_1, \cdots, x_n) {\rm の時}) \\ \psi_{m+1}(x_1, \cdots, x_n) & ({\rm 上記のいづれでも無い時}) \end{array}\right.$
${\rm は}\braces{ \psi_1, \cdots, \psi_{m+1}, \chi_{P_1}, \cdots, \chi_{P_m} }{\text -}{\rm 原始帰納的関数}$ が成り立つ。
${\cal D}$は関数の有限集合とする。
${\cal Q}$は述語の有限集合とする。
- $P {\rm は原始帰納的述語} \Rightarrow P {\rm は帰納的述語}$ が成り立つ。
- $P {\rm は}{\cal D}{\text -}{\rm 原始帰納的述語} \Rightarrow P {\rm は}{\cal D}{\text -}{\rm 帰納的述語}$ が成り立つ。
- $\left\{\begin{array}{} \varphi {\rm は}{\cal Q}{\text -}{\rm 帰納的関数} & {\rm かつ} \\ {\rm 任意の} Q \in {\cal Q} {\rm に対し、} Q {\rm は帰納的述語} & \end{array}\right. \Rightarrow \varphi {\rm は帰納的関数}$ が成り立つ。
- $\left\{\begin{array}{} \varphi {\rm は}{\cal Q}{\text -}{\rm 原始帰納的関数} & {\rm かつ} \\ {\rm 任意の} Q \in {\cal Q} {\rm に対し、} Q {\rm は原始帰納的述語} & \end{array}\right. \Rightarrow \varphi {\rm は原始帰納的関数}$ が成り立つ。
$P(y_1, \cdots, y_m)$を述語、$(\varphi_i(x_1, \cdots, x_n))_{i=1}^m$を関数の有限列とする。
$P(\varphi_1(x_1, \cdots, x_n), \cdots, \varphi_m(x_1, \cdots, x_n)) {\rm は}\braces{ \chi_P, \varphi_1, \cdots, \varphi_m }{\text -}{\rm 原始帰納的述語}$が成り立つ。
$P(x_1, \cdots, x_n), Q(x_1, \cdots, x_n)$を述語とする。
- $\neg P(x_1, \cdots, x_n) {\rm は}\braces{ P }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $P(x_1, \cdots, x_n) \lor Q(x_1, \cdots, x_n) {\rm は}\braces{ P, Q }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $P(x_1, \cdots, x_n) \land Q(x_1, \cdots, x_n) {\rm は}\braces{ P, Q }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $P(x_1, \cdots, x_n) \Rightarrow Q(x_1, \cdots, x_n) {\rm は}\braces{ P, Q }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $P(x_1, \cdots, x_n) \Leftrightarrow Q(x_1, \cdots, x_n) {\rm は}\braces{ P, Q }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $(\exi y)_{y \lt z} P(x_1, \cdots, x_n, y) {\rm は}\braces{ P }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
- $(\all y)_{y \lt z} P(x_1, \cdots, x_n, y) {\rm は}\braces{ P }{\text -}{\rm 原始帰納的述語}$ が成り立つ。
以下に定義される関数は、$\braces{ P }{\text -}{\rm 原始帰納的関数}$である。
- "$y \lt z \land P(x_1, \cdots, x_n, y)$を満たす$y$が存在する時はそのような$y$の最小値を、そのような$y$が存在しない時は$z$を値にとる"関数
$\mu y_{y \lt z} P(x_1, \cdots, x_n, y) \equ {\displaystyle \sum\limits_{w \lt z}} ( {\displaystyle \prod\limits_{y \leq w}} \chi_P(x_1, \cdots, x_n, y) )$ - $\begin{array}{@{}l@{}l@{}c@{}l@{}l@{}} \mu y_{y \leq z} & P(x_1, \cdots, x_n, y) & \equ & \mu y_{y \lt z+1} & P(x_1, \cdots, x_n, y) \\ \mu y_{w \lt y \lt z} & P(x_1, \cdots, x_n, y) & \equ & \mu y_{y \lt z \dot{-} (w+1)} & P(x_1, \cdots, x_n, y+w+1) + (w+1) \\ \mu y_{w \leq y \leq z} & P(x_1, \cdots, x_n, y) & \equ & \mu y_{y \lt (z \dot{-} w)+1} & P(x_1, \cdots, x_n, y+w) + w \end{array}$
$(\psi_i(x_1, \cdots, x_n))_{i=1}^{m+1}$を関数の有限列とする。
$(P_i(x_1, \cdots, x_n))_{i=1}^m$を述語の有限列とし、これらのどの2つをとっても同時に成立することは無いとする。 $\varphi(x_1, \cdots, x_n) :\equiv \left\{\begin{array}{@{}@{}} \psi_1(x_1, \cdots, x_n) & (P_1(x_1, \cdots, x_n) {\rm の時}) \\ \cdots & \cdots \\ \psi_m(x_1, \cdots, x_n) & (P_m(x_1, \cdots, x_n) {\rm の時}) \\ \psi_{m+1}(x_1, \cdots, x_n) & ({\rm 上記のいづれでも無い時}) \end{array}\right.$
${\rm は}\braces{ \psi_1, \cdots, \psi_{m+1}, \chi_{P_1}, \cdots, \chi_{P_m} }{\text -}{\rm 原始帰納的関数}$ が成り立つ。
原始帰納的関数、原始帰納的述語の例を複数挙げる。
- $a \equ b$
この表現関数は${\rm sg}(|a-b|)$である。 - $a \leq b$
この表現関数は${\rm sg}(a \dot{-} b)$である。 - $a \lt b$の表現関数は$\overline{{\rm sg}}(b \dot{-} a)$である。
- $l(z) \equ \mu x_{x \leq z} \parenth{ \exi y_{y \leq z} ( j(x,y) \equ z ) }$
- $r(z) \equ \mu y_{y \leq z} \parenth{ \exi x_{x \leq z} ( j(x,y) \equ z ) }$
- "$a$は$b$を割り切る"という述語$a | b$
$a | b :\Leftrightarrow \exi c_{1 \leq c \leq b} \parenth{ a \cdot c \equ b }$ - "$a$は素数である"という述語$pr(a)$
${\rm pr(a)} :\Leftrightarrow \all b_{1 \lt b \lt a} \neg \parenth{ b | a }$ - "$i+1$番目の素数"を与える関数
$\left\{\begin{array}{@{}l@{}c@{}l@{}} p_0 & \equ & 2 \\ p_{i+1} & \equ & \mu x_{x \leq p_i!+1} \parenth{ p_i \lt x \land {\rm pr(x)} } \end{array}\right.$ - "$a$を素因数分解した時の$p_i$の冪指数"を与える関数
$(a)_i \equ \left\{\begin{array}{@{}l@{}l@{}} 0 & \parenth{ a \equ 0 {\rm の時} } \\ \mu x_{x \lt a} \bracket{ p_i^x | a \land \neg \parenth{ p_i^{x+1} | a } } & \parenth{ a \neq 0 {\rm の時} } \end{array}\right.$ - "$a$を素因数分解した時の、$p_i$より小さい相異なる素因数の個数"を与える関数
$\left\{\begin{array}{@{}l@{}c@{}l@{}} {\rm lh}^*(0, a) & \equ & 0 \\ {\rm lh}^*(i+1, a) & \equ & \left\{\begin{array}{@{}l@{}l@{}} {\rm lh}^*(i, a) + 1 & \parenth{ p_i | a {\rm の時} } \\ {\rm lh}^*(i, a) & \parenth{ p_i | a {\rm の時} } \end{array}\right. \end{array}\right.$
"$a$を素因数分解した時の相異なる素因数の個数"を与える関数
${\rm lh}(a) \equ {\rm lh}^*(a, a)$ - $a * b \equ a \cdot {\displaystyle \prod\limits_{i \lt {\rm lh}(b)}} p_{{\rm lh}(a)+i}^{(b)_i}$
- $\left\{\begin{array}{@{}l@{}c@{}l@{}} j_1(x) & \equ & x \\ j_{n+1}(x_1, x_2, \cdots, x_{n+1}) & \equ & j(x_1, j_n(x_2, \cdots, x_{n+1})) \end{array}\right.$
- $\left\{\begin{array}{@{}l@{}c@{}l@{}} r^*(0, x) & \equ & x \\ r^*(n+1, x) & \equ & r(r^*(n, x)) \end{array}\right.$
- $[a]_i \equ l(r^*(i, a))$
$\bracket{ a \equ j_{n+1}(a_0, a_1, \cdots, a_{n-1}, 0) \Rightarrow [a]_i \equ \left\{\begin{array}{@{}l@{}l@{}} a_i & \parenth{ 0 \leq i \leq n-1 {\rm の時} } \\ 0 & \parenth{ n \leq i {\rm の時} } \end{array}\right. }$が成り立つ。 - ${\rm le}(a) \equ {\displaystyle \sum\limits_{i \lt a}} {\rm sg}([a]_i)$
$\bracket{\left\{\begin{array}{@{}l@{}l@{}} a \equ j_{n+1}(a_0, a_1, \cdots, a_{n-1}, 0) & {\rm かつ} \\ \all i \in \braces{ 0, \cdots, n-1 } \; a_i \gt 0 & \end{array}\right. \Rightarrow {\rm le}(a) \equ n }$が成り立つ。 - $\left\{\begin{array}{@{}l@{}c@{}l@{}} {\rm jp}(0, a, b) & \equ & b \\ {\rm jp}(n+1, a, b) & \equ & j({\rm le}(a), {\rm jp}(n, r(a), b)) \end{array}\right.$
- $a \# b \equ {\rm jp}({\rm le}(a), a, b)$
$\bracket{\begin{array}{@{}l@{}} a_0, \cdots, a_{m-1}, b_0, \cdots, b_{n-1} \gt 0 {\rm の時} \\ j_{m+1}(a_0, \cdots, a_{m-1}, 0) \# j_{n+1}(b_0, \cdots, b_{n-1}, 0) \equ j_{m+n+1}(a_0, \cdots, a_{m-1}, b_0, \cdots, b_{n-1}, 0) \end{array}}$が成り立つ。
$\varphi(y, x_1, \cdots, x_n)$を関数とする。
累積帰納法
$\psi(y, z, x_1, \cdots, x_n)$を関数とする。
$\varphi(y, x_1, \cdots, x_n) \equ \psi(y, \bar{\varphi}(y, x_1, \cdots, x_n), x_1, \cdots, x_n)$が成り立つように関数$\varphi$を構成できる。
$\varphi {\rm は}\braces{ \psi }{\text -}{\rm 原始帰納的関数}$が成り立つ。
帰納的定義(拡張版)
$(\psi_i(x_1, \cdots, x_n))_{i \equ 0}^n$を関数の有限列とする。$\chi(x,y_0, \cdots, y_{n+1}, x_1, \cdots, x_n)$を関数とする。
$\left\{\begin{array}{@{}l@{}c@{}l@{}} \varphi(0, x_1, \cdots, x_n) & \equ & \psi_0(x_1, \cdots, x_n) \\ \hfill \vdots \hfill & & \vdots \hfill \\ \varphi(n, x_1, \cdots, x_n) & \equ & \psi_n(x_1, \cdots, x_n) \\ \varphi(x+n+1, x_1, \cdots, x_n) & \equ & \chi(x, \varphi(x, x_1, \cdots, x_n), \cdots, \varphi(x+n, x_1, \cdots, x_n), x_1, \cdots, x_n) \end{array}\right.$
で定義される関数$\varphi$は$\braces{ \psi_0, \cdots, \psi_n, \chi }$-原始帰納的関数である。
$\left\{\begin{array}{@{}l@{}c@{}l@{}} \tilde{\varphi}(z, x_1, \cdots, x_n) & :\equ & {\displaystyle \prod\limits_{y \lt z}} p_y^{\varphi(y, x_1, \cdots, x_n)} \\ \bar{\varphi}(z, x_1, \cdots, x_n) & :\equ & {\displaystyle \prod\limits_{y \lt z}} p_y^{\varphi(y, x_1, \cdots, x_n)+1} \end{array}\right.$
- $\left\{\begin{array}{@{}l@{}} \varphi {\rm は}\braces{ \tilde{\varphi} }{\text -}{\rm 原始帰納的関数} \\ \tilde{\varphi} {\rm は}\braces{ \varphi }{\text -}{\rm 原始帰納的関数} \end{array}\right.$が成り立つ。
- $\left\{\begin{array}{@{}l@{}} \varphi {\rm は}\braces{ \bar{\varphi} }{\text -}{\rm 原始帰納的関数} \\ \bar{\varphi} {\rm は}\braces{ \varphi }{\text -}{\rm 原始帰納的関数} \end{array}\right.$が成り立つ。
累積帰納法
$\psi(y, z, x_1, \cdots, x_n)$を関数とする。
$\varphi(y, x_1, \cdots, x_n) \equ \psi(y, \bar{\varphi}(y, x_1, \cdots, x_n), x_1, \cdots, x_n)$が成り立つように関数$\varphi$を構成できる。
$\varphi {\rm は}\braces{ \psi }{\text -}{\rm 原始帰納的関数}$が成り立つ。
帰納的定義(拡張版)
$(\psi_i(x_1, \cdots, x_n))_{i \equ 0}^n$を関数の有限列とする。$\chi(x,y_0, \cdots, y_{n+1}, x_1, \cdots, x_n)$を関数とする。
$\left\{\begin{array}{@{}l@{}c@{}l@{}} \varphi(0, x_1, \cdots, x_n) & \equ & \psi_0(x_1, \cdots, x_n) \\ \hfill \vdots \hfill & & \vdots \hfill \\ \varphi(n, x_1, \cdots, x_n) & \equ & \psi_n(x_1, \cdots, x_n) \\ \varphi(x+n+1, x_1, \cdots, x_n) & \equ & \chi(x, \varphi(x, x_1, \cdots, x_n), \cdots, \varphi(x+n, x_1, \cdots, x_n), x_1, \cdots, x_n) \end{array}\right.$
で定義される関数$\varphi$は$\braces{ \psi_0, \cdots, \psi_n, \chi }$-原始帰納的関数である。
多重帰納的関数
原始帰納的関数のクラス${\cal F}$を次で定める：
2変数関数${\rm penum}(x, y)$を2重帰納法を用いて次で定める：
${\rm penum}(x, y) \equ \left\{\begin{array}{@{}l@{}l@{}} s(y) & \parenth{ x \equ 7m {\rm の時} } \\ l(y) & \parenth{ x \equ 7m+1 {\rm の時} } \\ r(y) & \parenth{ x \equ 7m+2 {\rm の時} } \\ 0(y) & \parenth{ x \equ 7m+3 {\rm の時} } \\ {\rm penum}(l(m), {\rm penum}(r(m), y)) & \parenth{ x \equ 7m+4 {\rm の時} } \\ \varphi_m(y) & \parenth{ x \equ 7m+5 {\rm の時} } \\ j({\rm penum}(l(m), y), {\rm penum}(r(m), y)) & \parenth{ x \equ 7m+6 {\rm の時} } \end{array}\right.$
ただし、$\varphi_m(y)$は$\left\{\begin{array}{@{}l@{}c@{}l@{}} \varphi_m(0) & \equ & {\rm penum}(l(m), 0) \\ \varphi_m(y+1) & \equ & {\rm penum}(r(m), \varphi_m(y)) \end{array}\right.$で定義された関数である。
- $s(x) \equ x+1, l(x), r(x), 0(x) \equ 0 \quad \in {\cal F}$
- $\psi(x), \chi(x) \in {\cal F}$ならば、
$\varphi(x) \equ j(\psi(x), \chi(x)), \varphi(x) \equ \psi(\chi(x)), \left\{\begin{array}{@{}l@{}c@{}l@{}} \varphi(0) & \equ & \psi(0) \\ \varphi(x+1) & \equ & \chi(\varphi(x)) \end{array}\right.$
で定義される$\varphi(x)$は、$\varphi(x) \in {\cal F}$ - $\varphi(x) \in {\cal F}$となる関数は、以上によって$\varphi(x) \in {\cal F}$となるものに限る。
2変数関数${\rm penum}(x, y)$を2重帰納法を用いて次で定める：
${\rm penum}(x, y) \equ \left\{\begin{array}{@{}l@{}l@{}} s(y) & \parenth{ x \equ 7m {\rm の時} } \\ l(y) & \parenth{ x \equ 7m+1 {\rm の時} } \\ r(y) & \parenth{ x \equ 7m+2 {\rm の時} } \\ 0(y) & \parenth{ x \equ 7m+3 {\rm の時} } \\ {\rm penum}(l(m), {\rm penum}(r(m), y)) & \parenth{ x \equ 7m+4 {\rm の時} } \\ \varphi_m(y) & \parenth{ x \equ 7m+5 {\rm の時} } \\ j({\rm penum}(l(m), y), {\rm penum}(r(m), y)) & \parenth{ x \equ 7m+6 {\rm の時} } \end{array}\right.$
ただし、$\varphi_m(y)$は$\left\{\begin{array}{@{}l@{}c@{}l@{}} \varphi_m(0) & \equ & {\rm penum}(l(m), 0) \\ \varphi_m(y+1) & \equ & {\rm penum}(r(m), \varphi_m(y)) \end{array}\right.$で定義された関数である。
- $\bracket{ {\rm 任意の1変数原始帰納的関数}\varphi(x){\rm に対して、} \varphi(x) \in {\cal F} }$ が成り立つ。
- $\Set{ {\rm 変数}x{\rm の関数penum}(n, x) }{ n \in {\mathbb N} } \equ \Set{ \varphi }{ \varphi {\rm は1変数原始帰納的関数} }$ が成り立つ。
- ${\rm penum}(x, y) {\rm は2変数}x, y{\rm の関数として原始帰納的関数ではない}$が成り立つ。
(原始)帰納的部分関数
帰納的部分関数を定義する図式
(原始)帰納的記述
$\varphi_1, \cdots, \varphi_l, \varphi$は部分関数とする。
$\varphi$は部分関数とする。
$P$は部分述語とする。
- 初期関数
- 後者関数:
$\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 }$
- 後者関数:
- 与えられた部分関数から得られる部分関数
- 合成:
$\psi$は$m$変数部分関数、$\chi_1, \cdots, \chi_m$は$n$変数部分関数とする。$\varphi(x_1, \cdots, x_n) :\simeq \psi(\chi_1(x_1, \cdots, x_n), \cdots, \chi_m(x_1, \cdots, x_n))$注意：$\psi(\chi_1(x_1, \cdots, x_n), \cdots, \chi_m(x_1, \cdots, x_n))$が定義されているとは、任意の$i \in \braces{1, \cdots, m}$に対し$\chi_i(x_1, \cdots, x_n)$が定義されていて、その値を$y_i$とすると、$\psi(y_1, \cdots, y_m)$が定義されているということである。
- 帰納的定義:
$\psi$は$n$変数部分関数、$\chi$は$n+2$変数部分関数とする。$\left\{\begin{array}{} \varphi(0, x_1, \cdots, x_n) & :\simeq & \psi(x_1, \cdots, x_n) \\ \varphi(x^\prime, x_1, \cdots, x_n) & :\simeq & \chi(x, \varphi(x, x_1, \cdots, x_n), x_1, \cdots, x_n) \\ \end{array}\right.$注意：例えば、$\varphi(a, x_1, \cdots, x_n)$が定義されるとは、$b \lt a$なる全ての$b$に対して、$\varphi(b, x_1, \cdots, x_n)$が定義されていなくてはならない。$\varphi(b, x_1, \cdots, x_n)$が定義されないような$b$が存在すれば、$b \lt a$なる全ての$a$に対し、$\varphi(a, x_1, \cdots, x_n)$は定義されないのである。
- $\mu$-作用素の適用もしくは最小化の操作:
$\psi$は$n+1$変数部分関数とする。
$\varphi(x_1, \cdots, x_n) :\simeq \mu y \bracket{ \psi(x_1, \cdots, x_n, y) \equ 0 }$注意：$\mu y \bracket{ \psi(x_1, \cdots, x_n, y) \equ 0 }$が定義され、その値が$a$であるとは、$b \lt a$なる全ての$b$に対して、$\psi(x_1, \cdots, x_n, b)$が定義され、かつ、$\psi(x_1, \cdots, x_n, b) \neq 0$であることを意味する。
- 合成:
(原始)帰納的記述
$\varphi_1, \cdots, \varphi_l, \varphi$は部分関数とする。
| $\varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての帰納的記述}$ | $:\Leftrightarrow$ |
| $\left\{\begin{array}{@{}@{}@{}} \left.\begin{array}{@{}@{}} {\rm 任意の}i \equ 1, \cdots, l{\rm に対して、} \\ \quad\left\{\begin{array}{@{}@{}@{}@{}} (1) & \varphi_i {\rm は初期関数} & {\rm または} \\ (2) & \left(\begin{array}{} j_1, \cdots, j_m \lt i {\rm が存在して} \\ \quad \varphi_i {\rm は部分関数} \varphi_{j_1}, \cdots, \varphi_{j_m} {\rm から得られる部分関数} \end{array}\right. \end{array}\right. \end{array}\right) & {\rm かつ} \\ \psi_l \equ \varphi & \end{array}\right.$ | |
| $\varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての原始帰納的記述}$ | $:\Leftrightarrow$ |
| $\left\{\begin{array}{@{}@{}@{}} \left.\begin{array}{@{}@{}} {\rm 任意の}i \equ 1, \cdots, l{\rm に対して、} \\ \quad\left\{\begin{array}{@{}@{}@{}@{}} (1) & \varphi_i {\rm は初期関数} & {\rm または} \\ (2) & \left(\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}\right. \end{array}\right. \end{array}\right) & {\rm かつ} \\ \psi_l \equ \varphi & \end{array}\right.$ | |
$\varphi$は部分関数とする。
| $\varphi$は帰納的部分関数 | $:\Leftrightarrow$ | $\left(\begin{array}{@{}@{}} {\rm 部分関数}\varphi_1, \cdots, \varphi_l{\rm が存在して、} \\ \quad \varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての帰納的記述} \end{array}\right.$ |
| $\varphi$は原始帰納的部分関数 | $:\Leftrightarrow$ | $\left(\begin{array}{@{}@{}} {\rm 部分関数}\varphi_1, \cdots, \varphi_l{\rm が存在して、} \\ \quad \varphi_1, \cdots, \varphi_l {\rm は}\varphi{\rm についての原始帰納的記述} \end{array}\right.$ |
$P$は部分述語とする。
| $P$は帰納的部分述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P {\rm は帰納的部分関数}$ |
| $P$は原始帰納的部分述語 | $:\Leftrightarrow$ | $P$の表現関数$\chi_P {\rm は原始帰納的部分関数}$ |
定理
$\varphi$は関数とする。$P$は述語とする。
$\left\{\begin{array}{@{}c@{}l@{}r@{}c@{}l@{}r@{}} (1) & \varphi {\rm は} & {\rm 帰納的関数} & \Rightarrow & \varphi {\rm は} & {\rm 帰納的部分関数} \\ (2) & \varphi {\rm は} & {\rm 原始帰納的関数} & \Rightarrow & \varphi {\rm は} & {\rm 原始帰納的部分関数} \\ (3) & P {\rm は} & {\rm 帰納的述語} & \Rightarrow & P {\rm は} & {\rm 帰納的部分述語} \\ (4) & P {\rm は} & {\rm 原始帰納的述語} & \Rightarrow & P {\rm は} & {\rm 原始帰納的部分述語} \end{array}\right.$が成り立つ。
$\left\{\begin{array}{@{}c@{}l@{}r@{}c@{}l@{}r@{}} (1) & \varphi {\rm は} & {\rm 帰納的関数} & \Rightarrow & \varphi {\rm は} & {\rm 帰納的部分関数} \\ (2) & \varphi {\rm は} & {\rm 原始帰納的関数} & \Rightarrow & \varphi {\rm は} & {\rm 原始帰納的部分関数} \\ (3) & P {\rm は} & {\rm 帰納的述語} & \Rightarrow & P {\rm は} & {\rm 帰納的部分述語} \\ (4) & P {\rm は} & {\rm 原始帰納的述語} & \Rightarrow & P {\rm は} & {\rm 原始帰納的部分述語} \end{array}\right.$が成り立つ。
