n番目の素数を返す関数は原始再帰関数である
参考文献
ぶっちゃけた話をするとこれの3章をほとんど書き直しているに過ぎない．
ただこの文書では形式的な自然数$ \Nと，普通の意味の自然数$ \mathcal{N}を明確に区別している
定義: 自然数
記号$ \mathtt{0,s}があったとき，次のように再帰的に定義されるものは自然数と呼ぶ． 0. $ \mathtt{0}は自然数である．
1. $ \mathtt{n}が自然数であるとき，$ \mathtt{s(n)}は自然数である．
なおカッコ$ (,)は単に見やすさのために使っている．
全ての自然数の集合を$ \Nで表す．
すなわち，$ \N = \{ \mathtt{0}, \mathtt{s(0)}, \mathtt{ss(0), \dots}\}である．
以後，↑の意味の自然数はタイプライタ体で書き，個数を表すときなどの普通の意味の自然数はそのままの字体で書く．
以降例示のために$ \tt s(0) = 1, s(1)=2,s(2)=3,s(3)=4,\dotsとしておく．
$ n個の自然数$ x_1,\dots,x_nを受け取り，1つの自然数を返すシステムは$ n変数関数と呼ぶ．
$ fが$ n変数関数であることは$ f:\N^n \to \Nとして表す．
$ fが$ n個の自然数$ \mathtt{x}_1,\dots,\mathtt{x}_nを受け取って出力$ \mathtt{y}を返すことを
$ f(\mathtt{x}_1,\dots,\mathtt{x}_n) = \mathtt{y}として表す．
また，明らかな場合は$ f(\vec{\mathtt{x}}) = \mathtt{y}として表す．
定義: 原始再帰関数
全ての自然数上の関数$ \N^n \to \Nのうち，次のものは原始再帰的関数と呼ばれる． 0. 後続関数: $ \mathsf{succ}: \N \to \N
$ \mathsf{succ}(\mathtt{n}) = \mathtt{s(n)}
1. 定数関数: 任意の自然数$ \mathtt{c}に対し，$ \mathsf{const}^n_\mathtt{c}: \N^n \to \N
$ \mathsf{const}^n_\mathtt{c}(\vec{x}) = \mathtt{c}
2. 射影関数: $ \mathsf{proj}^n_i: \N^n \to \N
$ \mathsf{proj}^n_i(\mathtt{x}_1,\dots,\mathtt{x}_n) = \mathtt{x}_i
3. 関数合成: 原始再帰関数$ f:\N^n \to \N, g:\N \to \Nに対して，$ \mathsf{comp}_{f,g}:\N^n \to \N
$ \mathsf{comp}_{f,g}(\vec{\mathtt{x}}) = g(f(\vec{\mathtt{x}}))
4. 原始再帰: 原始再帰関数$ f:\N^n \to \N, g:\N^{n+2} \to \Nに対して，$ \mathsf{prec}_{f,g}:\N^{n+1} \to \N
$ \mathsf{prec}_{f,g}(\vec{\mathtt{x}},\mathtt{0}) = f(\vec{\mathtt{x}})
$ \mathsf{prec}_{f,g}(\vec{\mathtt{x}}, \mathtt{s(n)}) = g(\vec{x},\mathtt{n},\mathsf{prec}_{f,g}(\vec{x},\mathtt{n}))
定義: ゼロ関数$ \mathsf{zero}^n(\vec{\mathtt{x}})
$ \mathsf{zero}^nは$ \mathsf{const}^n_\mathtt{0}の略記とする．
定義: 加算$ \mathsf{add}(\mathtt{x},\mathtt{y})/$ \mathtt{x}+\mathtt{y}
次で定義される原始再帰関数$ \mathsf{add}:\N^2\to\Nは加算と呼ばれる．
$ \mathsf{add}(\mathtt{x},\mathtt{0}) = \mathsf{proj}^2_1(\mathtt{x},\mathtt{0}) \Rightarrow \mathtt{0}
$ \mathsf{add}(\mathtt{x},\mathtt{s(n)}) = \mathtt{s}(\mathsf{proj}^3_3(\mathtt{x},\mathtt{n},\mathsf{add}(x,\mathtt{n}))) \Rightarrow \mathtt{s}(\mathsf{add}(x,\mathtt{n}))
$ \Rightarrowで，簡約化するとどうなるのかを表す．
長いので，以下$ \mathsf{add}(\mathtt{x},\mathtt{y})は$ \mathtt{x} + \mathtt{y}と表記する．
定義: 乗算$ \mathsf{mul}(\mathtt{x},\mathtt{y})/$ \mathtt{x}\times\mathtt{y}
次で定義される原始再帰関数$ \mathsf{mul}:\N^2\to\Nは乗算と呼ばれる．
$ \mathsf{mul}(\mathtt{x},\mathtt{0}) = \mathsf{zero}^2(\mathtt{x},\mathtt{0})
$ \mathsf{mul}(\mathtt{x},\mathtt{s(n)}) = \mathsf{add}(\mathsf{proj}^3_1(\mathtt{x},\mathtt{n},\mathsf{mul}(\mathtt{x},\mathtt{n})),\mathsf{proj}^3_3(\mathtt{x},\mathtt{n},\mathsf{mul}(\mathtt{x},\mathtt{n}))) \Rightarrow \mathtt{x} + \mathsf{mul}(\mathtt{x},\mathtt{n})
長いので，以下$ \mathsf{mul}(\mathtt{x},\mathtt{y})は$ \mathtt{x} \times \mathtt{y}と表記する．
注意: 射影関数と関数合成などの省略
乗算の時点でかなり長いので，定数関数，射影関数，関数合成などが明らかに自明なら省略する．
定義: 前者関数$ \mathsf{pred}(\mathtt{x})
次で定義される原始再帰関数$ \mathsf{pred}:\N\to\Nは前者関数と呼ばれる．
$ \mathsf{pred}(\mathtt{x},\mathtt{0}) = \mathsf{zero}^2(\mathtt{x},\mathtt{0}) \Rightarrow \mathtt{0}
$ \mathsf{pred}(\mathtt{x},\mathtt{s(n)}) = \mathsf{proj}^3_2(\mathtt{x},\mathtt{n},\mathsf{pred}(\mathtt{x},\mathtt{n})) \Rightarrow \mathtt{n}
定義: 補正付き減算$ \mathsf{msub}(\mathtt{x},\mathtt{y})/$ \mathtt{x} \ominus \mathtt{y} 次で定義される原始再帰関数$ \mathsf{msub}:\N^2\to\Nは補正付き減算と呼ばれる．
$ \mathsf{msub}(\mathtt{x},\mathtt{0}) = \mathtt{x}
$ \mathsf{msub}(\mathtt{x},\mathtt{s(n)}) = \mathsf{pred}(\mathsf{msub}(\mathtt{x},\mathtt{n}))
長いので，以下$ \mathsf{msub}(\mathtt{x},\mathtt{y})は$ \mathtt{x} \ominus \mathtt{y}と表記する．
例
$ \tt 3 \ominus 2 = 1
$ \tt 2 \ominus 3 = 0
定義: 階乗$ \mathsf{frac}(\mathtt{x}) / $ \mathtt{x}!
次で定義される原始再帰関数$ \mathsf{frac}:\N\to\Nは階乗と呼ばれる．
$ \mathsf{frac}(\mathtt{0}) = \mathsf{const}^1_\mathtt{1} (\mathtt{0}) \Rightarrow \mathtt{1}
$ \mathsf{frac}(\mathtt{s(n)}) = \mathsf{frac}(\mathtt{n}) \times \mathsf{n}
定義: 正数判定$ \mathsf{pos?}(\mathtt{x}) 次で定義される原始再帰関数$ \mathsf{pos?}:\N\to\Nは正数判定と呼ばれる．
$ \mathsf{pos?}(\mathtt{x}) = \mathtt{0}
$ \mathsf{pos?}(\mathtt{s(n)}) = \mathtt{1}
定義: ゼロ判定$ \mathsf{zero?}(\mathtt{x}) 次で定義される原始再帰関数$ \mathsf{zero?}:\N\to\Nはゼロ判定と呼ばれる．
$ \mathsf{zero}(\mathtt{x},\mathtt{0}) = \mathtt{1}
$ \mathsf{zero}(\mathtt{x},\mathtt{s(n)}) = \mathtt{0}
有界和
任意の原始再帰関数$ f:\N^{n+1} \to \Nに対し，次の関数$ \Sigma_f:\N^{n+1} \to \Nは$ fの$ \vec{\mathtt{x}}に対する有界和と呼ばれる．
$ \Sigma_f(\vec{\mathtt{x}}, \mathsf{0}) = \mathtt{0}
$ \Sigma_f(\vec{\mathtt{x}}, \mathtt{s(n)}) = \Sigma_f(\vec{\mathtt{x}},\mathtt{n}) + f(\vec{\mathtt{x}},\mathtt{n}) \Rightarrow f(\vec{x},\mathtt{0}) + f(\vec{x},\mathtt{1}) + \cdots +f(\vec{x},\mathtt{n})
有界積
任意の原始再帰関数$ f:\N^{n+1} \to \Nに対し，次の関数$ \Pi_f:\N^{n+1} \to \Nは$ fの$ \vec{\mathtt{x}}に対する有界積と呼ばれる．
$ \Pi_f(\vec{\mathtt{x}}, \mathsf{0}) = \mathtt{1}
$ \Pi_f(\vec{\mathtt{x}}, \mathtt{s(n)}) = \Pi_f(\vec{\mathtt{x}},\mathtt{n}) \times f(\vec{\mathtt{x}},\mathtt{n}) \Rightarrow f(\vec{x},\mathtt{0}) \times f(\vec{x},\mathtt{1}) \times \cdots \times f(\vec{x},\mathtt{n})
例
$ \Sigma_\mathsf{succ}(\mathtt{4}) = \mathsf{succ}(\mathtt{0}) + \mathsf{succ}(\mathtt{1}) + \mathsf{succ}(\mathtt{2}) + \mathsf{succ}(\mathtt{3}) = \mathtt{10}
$ \Sigma_\mathsf{add}(\mathtt{2},\mathtt{4}) = \mathsf{add}(\mathtt{2},\mathtt{0}) + \mathsf{add}(\mathtt{2},\mathtt{1}) + \mathsf{add}(\mathtt{2},\mathtt{2}) + \mathsf{add}(\mathtt{2},\mathtt{3}) = \mathtt{14}
$ \Pi_\mathsf{succ}(\mathtt{4}) = \mathsf{succ}(\mathtt{0}) \times \mathsf{succ}(\mathtt{1}) \times \mathsf{succ}(\mathtt{2}) \times \mathsf{succ}(\mathtt{3}) = \mathtt{24}
$ \N上の$ n項関係$ R \sube \N^nに対し，次で定まる関数$ \chi_R : \N^n \to \Nは特性関数と呼ぶ．
$ \chi_{R}(\mathtt{x_1,\dots,x_n}) = \mathtt{1} \implies (\mathtt{x_1,\dots,x_n}) \in R
$ Rは$ (\mathtt{x_1,\dots,x_n})で成立するという．
$ \chi_{R}(\mathtt{x_1,\dots,x_n}) = \mathtt{0} \implies (\mathtt{x_1,\dots,x_n}) \notin R
$ Rは$ (\mathtt{x_1,\dots,x_n})では成立しないという．
$ \N上の$ n項関係$ R \sube \N^nの特性関数$ \chi_R:\N^n\to\Nが原始再帰関数であるとき，$ Rは原始再帰的関係と呼ぶ． 系: 同値
「$ \mathtt{x}は$ \mathtt{y}と等しい」を表す2項関係$ \mathtt{x} = \mathtt{y}は原始再帰関数である．
実際，特性関数$ \chi_=(\mathtt{x,y}) = \mathsf{zero?}(\mathtt{x}\ominus\mathtt{y}) \times \mathsf{zero?}(\mathtt{y}\ominus\mathtt{x})を構成出来る．
なお，「$ \mathtt{y}は$ \mathtt{x}と等しい」というのは「$ \mathtt{x}と$ \mathtt{y}は同じ個数の$ \mathtt{s}を持っている」という意味である．
系: 大小比較
「$ \mathtt{y}は$ \mathtt{x}より大きい」を表す2項関係$ \mathtt{x} < \mathtt{y}は原始再帰関数である．
実際，特性関数$ \chi_<(\mathtt{x,y}) = \mathsf{pos?}(\mathtt{x}\ominus\mathtt{y})を構成出来る．
なお，「$ \mathtt{y}は$ \mathtt{x}より大きい」というのは「$ \mathtt{y}は$ \mathtt{x}より多くの$ \mathtt{s}を持っている」という意味である．
逆に，「$ \mathtt{y}は$ \mathtt{x}より小さい」というのは「$ \mathtt{x}は$ \mathtt{y}より多くの$ \mathtt{s}を持っている」という意味である．
系: 関係の論理演算
$ n項関係$ R,Sに対し，次の関係$ \lnot R,(R\land S),(R\lor S)を定める．
$ \lnot R(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})が成立しない
$ (R \land S)(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})と$ S(\vec{\mathtt{x}})のどちらも成立
$ (R \lor S)(\vec{\mathtt{x}})が成立$ \iff$ R(\vec{\mathtt{x}})と$ S(\vec{\mathtt{x}})の少なくともどちらか一方が成立
このとき，$ R,Sが原始再帰関係なら$ \lnot R,(R\land S),(R\lor S)も原始再帰関数である．実際，以下のように特性関数を構成出来る．
$ \chi_{\lnot R}(\vec{\mathtt{x}}) = \mathsf{zero?}(\chi_R(\vec{\mathtt{x}}))
$ \chi_{R \land S}(\vec{\mathtt{x}}) = \chi_R(\vec{\mathtt{x}}) \times \chi_S(\vec{\mathtt{x}})
$ \chi_{R \land S}(\vec{\mathtt{x}}) = \mathsf{pos?}(\chi_R(\vec{\mathtt{x}}) + \chi_S(\vec{\mathtt{x}}))
定義: 同値と大小比較に関する補助的な関係
補助的な関係をいくつか用意する．
$ n+1項関係$ Rと$ n個の自然数$ \vec{\mathtt{x}}に対して，次の$ n+1項関係$ \forall_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y}), \exists_{\mathtt{y} < \mathtt{m}}. R(\vec{\mathtt{x}},\mathtt{y})を定める．
なおここで自由変数は$ \vec{\mathtt{x}},\mathtt{m}であり$ \mathtt{y}は束縛変数である．
$ \forall_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y})が成立$ \iff$ \mathtt{m}より小さな全ての$ \mathtt{i}に対して$ R(\vec{x},\mathtt{i})が成立
$ \exists_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y})が成立$ \iff$ \mathtt{m}より小さなある$ \mathtt{i}で$ R(\vec{x},\mathtt{i})が成立
これらは$ Rと$ \vec{\mathtt{x}}に対しての有界量化と呼ばれる． このとき，$ Rが原始再帰関係なら$ \forall_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y}), \exists_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y})は原始再帰関係である．実際，以下のように特性関数を構成できる．
$ \chi_{\forall_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y})}(\vec{\mathtt{x}},\mathtt{m}) = \Pi_\mathsf{\chi_{R}}(\vec{\mathtt{x}},\mathtt{m})
$ \Rightarrow \chi_{R}(\vec{\mathtt{x}},\mathtt{0}) \times \chi_{R}(\vec{\mathtt{x}},\mathtt{1}) \times \cdots \times \chi_{R}(\vec{\mathtt{x}},\mathtt{m-1})
$ \chi_{\exists_{\mathtt{y} < \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y})}(\vec{\mathtt{x}},\mathtt{m}) = \mathsf{pos?} \left( \Sigma_\mathsf{\chi_{R}}(\vec{\mathtt{x}},\mathtt{m}) \right)
$ \Rightarrow \mathsf{pos?}\left( \chi_{R}(\vec{\mathtt{x}},\mathtt{0}) + \chi_{R}(\vec{\mathtt{x}},\mathtt{1}) + \cdots + \chi_{R}(\vec{\mathtt{x}},\mathtt{m-1}) \right)
なお，実際には$ \leqに拡張すると便利であり，それらも原始再帰関係である．
すなわち次のように$ n+1関係$ \forall_{\mathtt{y} \leq \mathtt{m}} R(\vec{\mathtt{x}},\mathtt{y}), \exists_{\mathtt{y} \leq \mathtt{m}} R(\vec{\mathtt{x}},\mathtt{y})を定める．
$ \forall_{\mathtt{y} \leq \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y}) \coloneqq \forall_{\mathtt{y} < \mathtt{m}} R(\vec{\mathtt{x}},\mathtt{y}) \land R(\vec{\mathtt{x}},\mathtt{m})
$ \exists_{\mathtt{y} \leq \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y}) \coloneqq \exists_{\mathtt{y} < \mathtt{m}} R(\vec{\mathtt{x}},\mathtt{y}) \lor R(\vec{\mathtt{x}},\mathtt{m})
$ \vec{\mathtt{x}}に対して有界量化の上界$ \mathtt{m}を計算する関数$ m(\vec{\mathtt{x}})が原始再帰関数であるならば$ Rに対して有界最小化を行うことが出来る．
系: いくつかの数論的関係
$ \mathsf{even}(\mathtt{x})：「$ \mathtt{x}は偶数である．」
すなわち，$ \mathtt{x}は$ \mathtt{s}を持たない（すなわち$ \mathtt{0}）か，偶数個の$ \mathtt{s}を持つ．
$ \exists_\mathtt{y<x}.\mathtt{(x = 2 \times y)}として記述できる．
$ \mathsf{div}(\mathtt{x,y})：「$ \mathtt{x}は$ \mathtt{y}を割り切る」
すなわち，$ \mathtt{x}は$ \mathtt{y}の約数個の$ \mathtt{s}を持つ．
$ \exists_\mathtt{z \leq y}.\mathtt{(y = x \times z)}として記述できる．
$ \mathsf{prime}(\mathtt{x})：「$ \mathtt{x}は素数である．」
$ \mathtt{x}は素数個の$ \mathtt{s}を持つ．
$ (2 \leq x) \land \lnot(\exists_{\mathtt{y<x}}.(\mathtt{y \neq 1} \land \mathsf{div}(\mathtt{y,x})))
ここで，$ x \leq yと$ x \neq yは以下の関係とする．もちろん原始再帰関係である．
$ \mathtt{x \leq y} \coloneqq (x < y) \lor (x = y)
$ \mathtt{x} \neq \mathtt{y} \coloneqq \lnot(\mathtt{x} = \mathtt{y})
定義: 場合分けによる定義
$ n項原始再帰関数$ f,gと$ n項原始再帰関係$ Rについて，次の関数$ hは原始再帰関数である．
$ h(\vec{\mathtt{x}}) = f(\vec{\mathtt{x}}): $ R(\vec{\mathtt{x}})が成立する
$ h(\vec{\mathtt{x}}) = g(\vec{\mathtt{x}}): $ R(\vec{\mathtt{x}})が成立しない
実際，$ h(\vec{\mathtt{x}}) = \chi_R(\vec{\mathtt{x}}) \times f(\vec{\mathtt{x}}) + \chi_{\lnot R}(\vec{\mathtt{x}}) \times g(\vec{\mathtt{x}})として構成可能．
長いので，$ h(\vec{\mathtt{x}}) = \text{if $R(\vec{\mathtt{x}})$ then $f(\vec{\mathtt{x}})$ else $g(\vec{\mathtt{x}})$}と略記する．
定義: 有界最小化
$ n+1項原始再帰関係$ Rと$ n個の自然数$ \vec{\mathtt{x}}に対して，次の$ n+1項関数$ \mu_\mathtt{y \leq m}.R(\vec{\mathtt{x}},\mathtt{y})は原始再帰関数である．
なおここで自由変数は$ \vec{\mathtt{x}},\mathtt{m}であり$ \mathtt{y}は束縛変数である．
$ \mu_{\mathtt{y} \leq \mathtt{m}}.R(\vec{\mathtt{x}},\mathtt{y}) = \mathtt{k}$ \iff
$ \mathtt{k}は$ \mathtt{m}より小さい$ \mathtt{y}のうち$ R(\vec{\mathtt{x}},\mathtt{y})を成立させる最小の$ \mathtt{y}．
ただしそのような$ \mathtt{y}が存在しないなら$ \mathtt{k = m}．
関数$ \mu_\mathtt{m \leq y}.R(\vec{\mathtt{x}},\mathtt{y})は$ Rと$ \vec{\mathtt{x}}に対しての有界最小化という． 実際，次のように$ \mu_Rは構成できる．
$ \mu_R(\vec{\mathtt{x}},\mathtt{0}) = \mathtt{0}
$ \mu_R(\vec{\mathtt{x}},\mathtt{s(m)}) = \text{if $\exists_{\mathtt{y \leq m}} R(\vec{\mathtt{x}},\mathtt{y})$ then $\mu(\vec{\mathtt{x}},\mathtt{y})$ else $\mathtt{s(m)}$}
有界量化と同様に，$ \vec{\mathtt{x}}に対して有界最小化の上界$ \mathtt{m}を計算する関数$ m(\vec{\mathtt{x}})が原始再帰関数であるならば$ Rに対して有界最小化を行うことが出来る．
$ p_nが$ n番目の素数なら，$ n+1番目の素数$ p_{n+1}は$ p_n!+1以下に存在する．
証明
$ p_n!+1の1ではない最小の約数を$ mとする．
$ p_n < m \leq p_n!+1が成り立つ．
$ p_n < m
階乗の定義より，$ p_n!+1は2以上$ p_n以下のいかなる数で割っても1余る．
割り切れたとしたら$ p_n+1以上の数で割っている．
$ m \leq p_n!+1
約数の定義より自明．
$ mは素数である．
$ p_n!+1は$ p_n以下の素数で割り切れないのだから，当然その約数も$ p_n以下の素数で割り切れない．
$ mは最小の約数である．
よって，$ mは$ p_{n+1}番目の素数である．
系: $ n番目の素数
$ n番目の素数個の$ \mathtt{s}を持つ自然数$ \mathtt{x}を返す関数$ \mathsf{p}:\N\to\Nは原始再帰関数である．
ただし素数は0番目から数えるとする．すなわち以下．
$ \mathsf{p}(\mathtt{0}) = \mathtt{2}
$ \mathsf{p}(\mathtt{1}) = \mathtt{3}
$ \mathsf{p}(\mathtt{2}) = \mathtt{5}
次のように構成する．
$ \mathsf{p}(\mathtt{0}) = \mathtt{2}
$ \mathsf{p}(\mathtt{s(n)}) = \mu_{\mathtt{y} \leq (\mathsf{p}(\mathtt{n})!+1)}.(\mathsf{p}(\mathtt{n}) < \mathtt{y} \land \mathsf{prime}(\mathtt{y}))
次の素数は$ p(\mathtt{n})! + 1以下に必ず存在する．
有界最小化の上界$ p(\mathtt{n})! + 1を計算する関数は原始再帰関数である．
例
$ \mathsf{p}(\mathtt{1}) = \mu_{y \leq \mathtt{3}}.(\mathtt{2} < \mathtt{y} \land \mathsf{prime}(\mathtt{y})) = \mathtt{3}
$ \mathsf{p}(\mathtt{2}) = \mu_{y \leq \mathtt{7}}.(\mathtt{3} < \mathtt{y} \land \mathsf{prime}(\mathtt{y})) = \mathtt{5}
$ \mathtt{7}より小さい$ \mathtt{y}のうち，$ \mathtt{3}より大きい素数で，最も小さなものは$ \mathtt{5}である．