関数の超限再帰的定義

任意の集合\(x\)の各々に対し、ただひとつの集合\(G(x)\)を返す規則\(G\)が与えられている*1。順序数\(\alpha\)ごとに、条件\(\psi_\alpha(f)\)を「\(f\)は\(\alpha\)を定義域とする関数であり、任意の\(\beta\in{\rm dom}f\)について\(f(\beta)=G(f\upharpoonright_\beta)\)が成り立つ」と定義する。

補題】\(\psi_\alpha\)を満たすものは\(\alpha\)ごとに一意に存在する。

(証明)超限帰納法による。\(\beta < \alpha\)なる任意の\(\beta\)の各々に対し、\(f^*_\beta\)は\(\psi_\beta\)を満たす唯一のものであると仮定する。\(f=\{\langle\beta,G(f^*_\beta)\rangle:\beta < \alpha\}\)とおけば、\(f\)は\(\alpha\)を定義域とする関数クラスとなっているから、置換公理のもとで集合をなす。これが\(\psi_\alpha\)を満たすことを示す。任意の\(\beta < \alpha\)をとり、さらに任意の\(\gamma < \beta\)をとる。\(f^*_\beta\upharpoonright_\gamma\)は\(\psi_\gamma\)を満たすから\(f^*_\gamma\)に一致する。\(f^*_\beta\upharpoonright_\gamma=f^*_\gamma\)の両辺に\(G\)を作用させれば\(f^*_\beta(\gamma)=f(\gamma)\)、これが任意の\(\gamma < \beta\)で成り立つことから\(f^*_\beta=f\upharpoonright_\beta\)である。再び両辺に\(G\)を作用させると\(f(\beta)=G(f\upharpoonright_\beta)\)を得る。
次に一意性を示すため、\(\psi_\alpha(f')\)を仮定して\(f'=f\)を導く。任意の\(\beta < \alpha\)をとれば、\(f'\upharpoonright_\beta\)は\(\psi_\beta\)を満たすから\(f^*_\beta\)に一致する。\(f'\upharpoonright_\beta=f^*_\beta\)の両辺に\(G\)を作用させれば\(f'(\beta)=f(\beta)\)を得る。■

任意の順序数の各々\(\alpha\)に対し、\(\psi_\alpha\)を満たす唯一のものを改めて\(f^*_\alpha\)と書くことにする。

【定理】順序数\(\alpha\)に対し\(G(f^*_\alpha)\)を与える規則を\(F\)とすれば、\(F(\alpha)=G(F\upharpoonright_\alpha)\)が成り立つ。ここで\(F\upharpoonright_\alpha\)とは\(\{\langle\gamma,F(\gamma)\rangle:\gamma < \alpha\}\)を意味し、これは置換公理により集合をなしている。
(証明)任意の順序数\(\alpha\)をとると、補題の証明と同様にして\(f^*_\alpha=F\upharpoonright_\alpha\)を得るから、この両辺に\(G\)を作用させれば\(F(\alpha)=G(F\upharpoonright_\alpha)\)となる。■

*1:規則\(G\)の実体は、\(\forall x\exists!y[G(x,y)]\)を満たす述語\(G(x,y)\)である。