再帰定理 - y_bonten's blogを簡明に改良した。
『数学のロジックと集合論』p77、定理2.10の証明を、自分で書き直してみた。
\(m\in\mathbb{N}\)と写像\(g:\mathbb{N}\to\mathbb{N}\)が与えられている。\(k\in\mathbb{N}\)ごとに条件\(\psi_k(h)\)を「\(h\)が以下のすべてを満たすこと」と定義する。
・\(h:\mathbb{N}\to\mathbb{N}\)は\(\{0,1,\ldots,k\}\)を定義域とする部分写像である
・\(h(0)=m\)
・\(x'\in{\rm dom}(h)\)ならば\(h(x')=g(h(x))\)
【補題】各々の\(k\in\mathbb{N}\)に対し、\(\psi_k\)を満たすものが一意に存在する。
（証明）\(k\)についての帰納法による。まず\(\{\langle 0,m\rangle\}\)は\(\psi_0\)を満たしている。一意性を示すために\(\psi_0(h)\)を仮定すると、\(h(0)=m\)すなわち\(\langle 0,m\rangle\in h\)であり、\(h\)は定義域を\(\{0\}\)とする部分写像であるから、これ以外の要素を持たず、\(h=\{\langle 0,m\rangle\}\)となる。
次に\(k\in\mathbb{N}\)に対し、\(h^*_k\)が\(\psi_k\)を満たす唯一のものであると仮定し、\(\psi_{k'}\)を満たすものが一意に存在することを示す。\(h^*_k\)に\(\langle k',g(h^*_k(k))\rangle\)を付け加えたものを\(h_{k'}\)とすれば、これは\(\psi_{k'}\)を満たしている。一意性を示すために\(\psi_{k'}(h)\)を仮定し、\(h=h_{k'}\)を導く。\(h\upharpoonright_{\leq k}\)は\(\psi_k\)を満たしているから\(h^*_k\)に一致し、したがって\(h\upharpoonright_{\leq k}=h_{k'}\upharpoonright_{\leq k}\)である。特に\(h(k)=h_{k'}(k)\)が成り立つので、両辺に\(g\)を作用させると\(h(k')=h_{k'}(k')\)も得られる。■
各\(k\in\mathbb{N}\)に対し\(\psi_k\)を満たす唯一のものを\(h^*_k\)とおく。
【定理】\(f=\{\langle k,h^*_k(k)\rangle:k\in\mathbb{N}\}\)は、以下をともに満たすような唯一の全域写像\(:\mathbb{N}\to\mathbb{N}\)である。
・\(f(0)=m\)
・任意の\(n\in\mathbb{N}\)に対し、\(f(n')=g(f(n))\)
（証明）\(f\)は\(\mathbb{N}\)から\(\mathbb{N}\)への全域写像であり、\(f(n)=h^*_n(n)\)であるから、\(f(0)=h^*_0(0)=m\)である。任意の\(n\in\mathbb{N}\)をとると、\(h^*_{n'}\upharpoonright_{\leq n}\)は\(\psi_n\)を満たすゆえ\(h^*_n\)に一致するから\(h^*_{n'}(n)=h^*_{n'}\upharpoonright_{\leq n}(n)=h^*_{n}(n)\)、この最左辺と最右辺に\(g\)を作用させれば\(h^*_{n'}(n')=g(h^*_n(n))\)すなわち\(f(n')=g(f(n))\)となる。一意性を示すため、全域写像\(F:\mathbb{N}\to\mathbb{N}\)が同じ条件を満たすと仮定し、\(F=f\)を帰納法により示す。まず\(F(0)=m=f(0)\)である。\(F(k)=f(k)\)と仮定すると、両辺に\(g\)を作用させることにより\(F(k')=f(k')\)を得る。■
