再帰的定義

一意性. $f,f'$ がともに条件を満たすとし、$A:=\{n\in N\mid f(n)=f'(n)\}$ とおく。$f(0_N)=a=f'(0_N)$ なので $0_N\in A$ である。$n\in A$ なら $f(s(n))=g(f(n))=g(f'(n))=f'(s(n))$ なので $s(n)\in A$ である。条件 3 により $A=N$、すなわち $f=f'$ である。
存在. 直積 $N\times X$ の部分集合 $R$ が次の 2 条件を満たすとき、$R$ を 閉じている ということにする。
(a) $(0_N,a)\in R$。
(b) $(n,x)\in R$ ならば $(s(n),g(x))\in R$。
$N\times X$ 自身は閉じている。閉じている部分集合すべての共通部分を $F$ とすると、$F$ も (a)(b) を満たすので閉じており、閉じている部分集合の中で最小である。
$F$ が写像のグラフであること、すなわち各 $n\in N$ に対して $(n,x)\in F$ となる $x\in X$ がちょうど 1 つあることを示す。そのような $n$ の全体を $A$ とし、条件 3 を使う。

• $0_N\in A$：(a) により $(0_N,a)\in F$ である。$b\neq a$ で $(0_N,b)\in F$ となるものがあったとし、$F':=F\setminus\{(0_N,b)\}$ とおく。$F'$ は $(0_N,a)$ を含む。$(n,x)\in F'$ なら $(s(n),g(x))\in F$ であり、条件 1 より $s(n)\neq0_N$ なので $(s(n),g(x))\neq(0_N,b)$、すなわち $(s(n),g(x))\in F'$ である。よって $F'$ は閉じているが、$F$ より真に小さく、$F$ の最小性に反する。
• $n\in A$ なら $s(n)\in A$：$(n,x)\in F$ となる唯一の $x$ をとる。(b) により $(s(n),g(x))\in F$ である。$y\neq g(x)$ で $(s(n),y)\in F$ となるものがあったとし、$F':=F\setminus\{(s(n),y)\}$ とおく。条件 1 より $s(n)\neq0_N$ なので $(0_N,a)\in F'$ である。$(m,z)\in F'$ とする。$s(m)\neq s(n)$ なら $(s(m),g(z))\in F'$ である。$s(m)=s(n)$ なら条件 2 より $m=n$ であり、$n\in A$ から $z=x$、よって $g(z)=g(x)\neq y$ なので、やはり $(s(m),g(z))\in F'$ である。したがって $F'$ は閉じていて $F$ より真に小さく、矛盾する。
  条件 3 により $A=N$ である。そこで $f(n)$ を $(n,x)\in F$ となる唯一の $x$ と定めれば、$f\colon N\to X$ は写像であり、(a) から $f(0_N)=a$、(b) を $(n,f(n))\in F$ に使うと $(s(n),g(f(n)))\in F$ なので $f(s(n))=g(f(n))$ である。$\square$

段数を値の中に持ち運ぶ。$Y:=\mathbb{N}\times X$、$b:=(0,a)\in Y$、$G\colon Y\to Y$、$G(n,x):=(n+1,h(n,x))$ とおく。thm-recdef-recursion により $F(0)=b$、$F(n+1)=G(F(n))$ を満たす $F\colon\mathbb{N}\to Y$ がある。$F(n)=(p(n),f(n))$ と成分に分ける。$p(0)=0$、$p(n+1)=p(n)+1$ なので、帰納法で $p(n)=n$ がすべての $n$ で成り立つ。したがって $f(0)=a$、$f(n+1)=h(p(n),f(n))=h(n,f(n))$ である。
一意性：$f,f'$ がともに条件を満たせば、$f(0)=f'(0)$ であり、$f(n)=f'(n)$ なら $f(n+1)=h(n,f(n))=h(n,f'(n))=f'(n+1)$ なので、帰納法で $f=f'$ である。$\square$

「それまでの値の列」を 1 つの値として再帰する。列 $u=(u_0,\dots,u_{n-1})$ の末尾に $G(u)$ を付け加えた列 $(u_0,\dots,u_{n-1},G(u))$ を $\Phi(u)$ とおくと、$\Phi\colon X^{<\mathbb{N}}\to X^{<\mathbb{N}}$ は写像である。thm-recdef-recursion により
$$ U(0)=(),\qquad U(n+1)=\Phi\bigl(U(n)\bigr) $$
を満たす $U\colon\mathbb{N}\to X^{<\mathbb{N}}$ がある。帰納法により $U(n)$ の長さは $n$ であり、$U(n+1)$ は $U(n)$ の末尾に $G(U(n))$ を付けた列である。そこで $f(n):=G(U(n))$ と定める。
$U(n)=f|_n$ を帰納法で示す。$n=0$ では両辺とも空列である。$U(n)=f|_n$ なら、$U(n+1)$ は $f|_n$ の末尾に $G(U(n))=f(n)$ を付けた列、すなわち $f|_{n+1}$ である。したがって $f(n)=G(U(n))=G(f|_n)$ がすべての $n$ で成り立つ。
一意性：$f,f'$ がともに条件を満たすとして、数学的帰納法 の記事の定理「強い帰納法」を使う。$k< n$ のすべての $k$ で $f(k)=f'(k)$ なら $f|_n=f'|_n$ なので $f(n)=G(f|_n)=G(f'|_n)=f'(n)$ である。よってすべての $n$ で $f(n)=f'(n)$ である。$\square$

まず次を確かめる。組 $(N,0_N,s)$ と $(M,0_M,t)$ がどちらも「再帰の性質」（thm-recdef-recursion の結論）をもつなら、$F(0_N)=0_M$、$F\circ s=t\circ F$ を満たす $F$ はただ 1 つあり、全単射である。
$N$ の再帰の性質を $X=M$、$a=0_M$、$g=t$ に使うと、そのような $F\colon N\to M$ がただ 1 つある。同様に $M$ の再帰の性質から、$G(0_M)=0_N$、$G\circ t=s\circ G$ を満たす $G\colon M\to N$ がある。合成 $G\circ F\colon N\to N$ は
$$ (G\circ F)(0_N)=G(0_M)=0_N,\qquad (G\circ F)\circ s=G\circ t\circ F=s\circ(G\circ F) $$
を満たす。恒等写像 $\mathrm{id}_N$ も $\mathrm{id}_N(0_N)=0_N$、$\mathrm{id}_N\circ s=s\circ\mathrm{id}_N$ を満たす。$N$ の再帰の性質を $X=N$、$a=0_N$、$g=s$ に使うと、この 2 つの条件を満たす写像はただ 1 つなので $G\circ F=\mathrm{id}_N$ である。同様に $F\circ G=\mathrm{id}_M$ であり、$F$ は全単射で $G$ がその逆写像である。
1：thm-recdef-recursion により Peano 構造は再帰の性質をもつので、上のことから従う。
2：この記事の冒頭と同じく、通常の自然数 $(\mathbb{N},0,s)$ が Peano 構造であることを前提にする（集合論の中での構成は 自然数 の記事の例「von Neumann自然数」と 帰納的集合 の記事を参照）。$(\mathbb{N},0,s)$ は thm-recdef-recursion により再帰の性質をもつ。仮定から $(N,0_N,s)$ も再帰の性質をもつので、上のことから $F(0)=0_N$、$F(n+1)=s(F(n))$ を満たす全単射 $F\colon\mathbb{N}\to N$ がある。Peano 構造の 3 条件は全単射 $F$ で $\mathbb{N}$ から $N$ に移る。条件 1：$0_N=s(y)$ となる $y$ があれば、$y=F(k)$ として $F(0)=0_N=s(F(k))=F(k+1)$、$F$ の単射性から $0=k+1$ となり矛盾する。条件 2：$s(F(k))=s(F(l))$ なら $F(k+1)=F(l+1)$ より $k=l$、よって $F(k)=F(l)$ である。条件 3：$0_N\in A\subset N$、$s(A)\subset A$ なら、$F^{-1}(A)$ は $0$ を含み、$k\in F^{-1}(A)$ なら $F(k+1)=s(F(k))\in A$ なので $k+1\in F^{-1}(A)$ である。$\mathbb{N}$ の条件 3 から $F^{-1}(A)=\mathbb{N}$、$F$ が全射なので $A=N$ である。$\square$