※このエントリは古くなっています。より簡明な証明が
http://y-bonten.hatenablog.com/entry/2016/06/16/142914
にあります。
『数学のロジックと集合論』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}\)は\(k'=\{0,1,\ldots,k\}\)を定義域とする部分写像である
・\(h(0)=m\)
・\(x'\in k'\)ならば\(h(x')=g(h(x))\)
【補題】各々の\(k\in\mathbb{N}\)に対し、\(\psi_k(h)\)を満たす\(h\)が一意に存在する。
（証明）\(k\)についての帰納法による。まず\(\{\langle 0,m\rangle\}\)は\(\psi_0\)を満たしている。\(\psi_0(h)\)を仮定すると、\(h(0)=m\)すなわち\(\langle 0,m\rangle\in h\)であり、\(h\)は定義域を\(0'=\{0\}\)とする部分写像であるから、これ以外の要素を持たず、\(h=\{\langle 0,m\rangle\}\)となる。したがって\(\{\langle 0,m\rangle\}\)は\(\psi_0\)を満たす唯一のものである。
次に\(k\in\mathbb{N}\)に対し、\(h_k\)が\(\psi_k\)を満たす唯一のものであると仮定し、\(\psi_{k'}\)を満たすものが一意に存在することを示す。\(h_k\)に\(\langle k',g(h_k(k))\rangle\)を付け加えて定義域を\(k''\)に拡大したものを\(h_{k'}\)とすれば、これは\(\psi_{k'}\)を満たしている。一意性を示すために\(\psi_{k'}(h)\)を仮定し、\(h=h_{k'}\)を導く。\(h\)の定義域\(k''\)を\(k'\)に制限したもの、すなわち\(\{0,1,\ldots,k,k'\}\)から\(k'\)を除いたものを考えると、これは\(\psi_k\)を満たしているから\(h_k\)に一致する。したがって\(h(k)=h_k(k)\)だから、\(h(k')=g(h(k))=g(h_k(k))\)となり、\(h\)と\(h_{k'}\)は一致する。■
各\(k\in\mathbb{N}\)に対し\(\psi_k\)を満たす唯一のものを\(h_k\)とおく。
【補題】任意の\(p,q\in\mathbb{N}\)に対し、\(p\leq q\)ならば\(h_q(p)=h_p(p)\)である。
（証明）\(h_q\)の定義域\(q'\)を\(p'\)に制限したものは\(\psi_p\)を満たし、したがって\(h_p\)に一致するから、\(h_q(p)=h_p(p)\)となる。■
【定理】\(\displaystyle f=\bigcup_{k\in\mathbb{N}}h_k\)は、以下をともに満たすような唯一の全域写像\(:\mathbb{N}\to\mathbb{N}\)である。
・\(f(0)=m\)
・任意の\(n\in\mathbb{N}\)に対し、\(f(n')=g(f(n))\)
（証明）任意の\(n\in\mathbb{N}\)をとる。\(k\in\mathbb{N}\)に対し、\(k < n\)のとき\(n\)は\(h_k\)の定義域に属さず、\(n\leq k\)のとき前補題から\(h_k(n)=h_n(n)\)である。したがって\(\langle n,y\rangle\in f\)を満たす\(y\in\mathbb{N}\)は\(h_n(n)\)のみに定まる。よって\(f\)は\(\mathbb{N}\)から\(\mathbb{N}\)への全域写像であり、\(f(n)=h_n(n)\)と書ける。すると\(f(0)=h_0(0)=m\)である。また\(f(n')=h_{n'}(n')=g(h_{n'}(n))\)および\(g(f(n))=g(h_n(n))\)であり、前補題により両者は等しくなる。
一意性を示すため、全域写像\(f^*:\mathbb{N}\to\mathbb{N}\)が同じ条件を満たすと仮定し、\(f^*=f\)を帰納法により示す。まず\(f^*(0)=m=f(0)\)である。\(f^*(k)=f(k)\)と仮定すると、\(f^*(k')=g(f^*(k))=g(f(k))=f(k')\)が従う。■
