超限再帰

$\mu:=\min(\delta,\delta')$ とし、$D:=\{\beta<\mu\mid t(\beta)\neq s(\beta)\}$ とおく。これは順序数 $\mu$ の部分集合として分出公理で作れる集合である。$D\neq\emptyset$ と仮定すると、順序数の集合は最小元をもつので（順序数の「性質」節、命題「順序数の集まりの整列性と上限」）、$D$ の最小元 $\beta$ がある。最小性から $\gamma<\beta$ ではすべて $t(\gamma)=s(\gamma)$、すなわち $t|_\beta=s|_\beta$ である。$\mathbf{G}$ は各入力にただ一つの値を返すので
$$ t(\beta)=\mathbf{G}(t|_\beta)=\mathbf{G}(s|_\beta)=s(\beta) $$
となり、$\beta\in D$ に反する。よって $D=\emptyset$ である。$\delta=\delta'$ のときは定義域も一致するので $t=s$ となる。$\square$

長さ $\delta$ の計算が存在しない順序数 $\delta$ があると仮定する。超限帰納法の「順序数上の原理」節の命題「全順序数への拡張」と同じく、そのような $\delta$ の一つ $\delta_1$ をとり、$\delta_1+1$ の中の反例の集合の最小元を考えれば、長さ $\delta$ の計算が存在しない最小の順序数 $\delta$ がとれる。最小性により、$\eta<\delta$ ならば長さ $\eta$ の計算が存在し、lem-trec-agree によりそれはただ一つである。これを $t_\eta$ と書く。$\delta$ の種類で場合を分ける。
$\delta=0$ の場合。 空関数が長さ $0$ の計算なので、仮定に反する。
$\delta=\eta+1$ の場合。 $t:=t_\eta\cup\{(\eta,\mathbf{G}(t_\eta))\}$ とおく。$\eta$ は $t_\eta$ の定義域 $\eta$ に属さないので $t$ は定義域 $\eta+1$ の関数である。$\beta<\eta$ では $t|_\beta=t_\eta|_\beta$ なので $t(\beta)=t_\eta(\beta)=\mathbf{G}(t_\eta|_\beta)=\mathbf{G}(t|_\beta)$ である。$\beta=\eta$ では $t|_\eta=t_\eta$ なので $t(\eta)=\mathbf{G}(t_\eta)=\mathbf{G}(t|_\eta)$ である。よって $t$ は長さ $\delta$ の計算であり、仮定に反する。
$\delta$ が極限順序数の場合。 各 $\eta<\delta$ に $t_\eta$ を対応させる規則は「$t$ は長さ $\eta$ の計算である」という論理式で定まり、値はただ一つである。したがって置換公理により $T:=\{t_\eta\mid\eta<\delta\}$ は集合であり、和集合公理により $t:=\bigcup T$ も集合である。
$t$ は関数である。実際 $(\beta,y),(\beta,y')\in t$ なら $(\beta,y)\in t_\eta$、$(\beta,y')\in t_{\eta'}$ となる $\eta,\eta'<\delta$ があり、lem-trec-agree により $y=t_\eta(\beta)=t_{\eta'}(\beta)=y'$ である。$t$ の定義域は $\bigcup_{\eta<\delta}\eta$ であり、$\delta$ が極限順序数なので、これは $\delta$ に等しい（$\beta<\delta$ なら $\beta<\beta+1<\delta$ で $\beta\in\beta+1$、逆に $\eta<\delta$ の元は $\delta$ の元）。
最後に計算の条件を確かめる。$\beta<\delta$ とすると $\beta+1<\delta$ であり、$t_{\beta+1}\subset t$ と定義域の比較から $t|_{\beta+1}=t_{\beta+1}$、したがって $t|_\beta=t_{\beta+1}|_\beta$ である。よって
$$ t(\beta)=t_{\beta+1}(\beta)=\mathbf{G}(t_{\beta+1}|_\beta)=\mathbf{G}(t|_\beta) $$
であり、$t$ は長さ $\delta$ の計算である。これも仮定に反する。
どの場合も矛盾が生じたので、すべての順序数 $\delta$ について長さ $\delta$ の計算が存在する。$\square$

定義。 各順序数 $\delta$ について、長さ $\delta$ の計算が lem-trec-exist により存在し、lem-trec-agree によりただ一つである。これを $t_\delta$ と書く。集合 $x$ と $y$ について

• $x$ が順序数であり、$x+1$ を長さとする計算 $t$ があって $t(x)=y$ である、または
• $x$ は順序数でなく $y=\emptyset$ である
  という論理式を $\psi(x,y)$ とおく。上の存在と一意性から、どの $x$ に対しても $\psi(x,y)$ を満たす $y$ はただ一つであり、$\psi$ はクラス関数 $\mathbf{F}$ を定める。順序数 $\alpha$ では $\mathbf{F}(\alpha)=t_{\alpha+1}(\alpha)$ である。

制限が計算に一致すること。 順序数 $\alpha$ と $\beta<\alpha$ をとる。$t_{\beta+1}$ と $t_\alpha$ はともに計算で $\beta<\min(\beta+1,\alpha)$ なので、lem-trec-agree により $\mathbf{F}(\beta)=t_{\beta+1}(\beta)=t_\alpha(\beta)$ である。よって $\mathbf{F}|_\alpha=t_\alpha$ であり、特に $\mathbf{F}|_\alpha$ は集合である。
再帰式。 順序数 $\alpha$ について、$t_{\alpha+1}$ が計算であることと $t_{\alpha+1}|_\alpha=t_\alpha=\mathbf{F}|_\alpha$ から
$$ \mathbf{F}(\alpha)=t_{\alpha+1}(\alpha)=\mathbf{G}(t_{\alpha+1}|_\alpha)=\mathbf{G}(\mathbf{F}|_\alpha) $$
である。
一意性。 $\mathbf{F}'$ もすべての順序数で $\mathbf{F}'(\alpha)=\mathbf{G}(\mathbf{F}'|_\alpha)$ を満たすとする（$\mathbf{F}'|_\alpha$ は置換公理により集合である）。主張 $P(\alpha)$：「$\mathbf{F}'(\alpha)=\mathbf{F}(\alpha)$」を超限帰納法で示す。すべての $\beta<\alpha$ で $P(\beta)$ が成り立つとすると $\mathbf{F}'|_\alpha=\mathbf{F}|_\alpha$ なので、$\mathbf{F}'(\alpha)=\mathbf{G}(\mathbf{F}'|_\alpha)=\mathbf{G}(\mathbf{F}|_\alpha)=\mathbf{F}(\alpha)$ である。超限帰納法の「順序数上の原理」節の命題「全順序数への拡張」により、すべての順序数 $\alpha$ で $P(\alpha)$ が成り立つ。$\square$

集合 $t$ に対し、$\mathbf{G}(t)$ を次で定める。$t=\emptyset$ なら $a$。$t$ が定義域 $\eta+1$（$\eta$ は順序数）の関数なら $\mathbf{S}(t(\eta))$。$t$ が定義域が $0$ でない極限順序数の関数なら $\mathbf{L}(t)$。それ以外なら $\emptyset$。これらの場合は互いに排他的で、各場合の条件は論理式で書けるので、$\mathbf{G}$ はクラス関数である。thm-trec-main による $\mathbf{F}$ は $\mathbf{F}(0)=\mathbf{G}(\emptyset)=a$、$\mathbf{F}(\alpha+1)=\mathbf{G}(\mathbf{F}|_{\alpha+1})=\mathbf{S}(\mathbf{F}(\alpha))$、$\mathbf{F}(\lambda)=\mathbf{G}(\mathbf{F}|_\lambda)=\mathbf{L}(\mathbf{F}|_\lambda)$ を満たす。逆に三式を満たすクラス関数は、順序数が $0$・後続順序数・極限順序数のどれか一つであることから、すべての順序数 $\alpha$ で $\mathbf{F}'(\alpha)=\mathbf{G}(\mathbf{F}'|_\alpha)$ を満たすので、主定理の一意性により順序数上で $\mathbf{F}$ と一致する。$\square$

$S$ は $\mathcal{P}(\Omega\times A)$ から分出公理で作れる集合である。$t\in S$ なら $\mathbf{G}(t):=g(t)$、それ以外なら $\mathbf{G}(t):=\emptyset$ とおき、thm-trec-main の $\mathbf{F}$ をとる。$\alpha<\Omega$ について $\mathbf{F}(\alpha)\in A$ を超限帰納法で示す。$\beta<\alpha$ で $\mathbf{F}(\beta)\in A$ なら $\mathbf{F}|_\alpha$ は $\alpha$ から $A$ への関数で $\alpha<\Omega$ なので $\mathbf{F}|_\alpha\in S$、よって $\mathbf{F}(\alpha)=g(\mathbf{F}|_\alpha)\in A$ である。$f:=\mathbf{F}|_\Omega$ が求める写像である。別の $f'$ が同じ条件を満たせば、$f'(\alpha)=f(\alpha)$ を $\alpha<\Omega$ についての超限帰納法で示せる（prf-trec-main の一意性と同じ論法）。$\square$

順序数の「性質」節の定理「整列集合の順序数による表現」により、順序数 $\theta$ と順序同型写像 $\pi\colon W\to\theta$ がある。$\pi$ は始切片 $W_{< x}$ を始切片 $\pi(x)$ の上へ写す。$\beta<\theta$ と関数 $u\colon\beta\to A$ に対し、$x:=\pi^{-1}(\beta)$ として $g'(u):=g(u\circ\pi|_{W_{< x}})$ とおく。cor-trec-set-version を $\Omega=\theta$、$g'$ に適用して $f'\colon\theta\to A$ を得て、$f:=f'\circ\pi$ とおく。$x\in W$、$\beta=\pi(x)$ とすると $f|_{W_{< x}}=f'|_\beta\circ\pi|_{W_{< x}}$ なので
$$ f(x)=f'(\beta)=g'(f'|_\beta)=g(f'|_\beta\circ\pi|_{W_{< x}})=g(f|_{W_{< x}}) $$
である。一意性は、条件を満たす $f$ から $f\circ\pi^{-1}$ を作ると cor-trec-set-version の条件を満たすので、その一意性に帰着する。$\square$