整礎関係

1．循環があれば、$S=\{x_0,\dots,x_{n-1}\}$ の各元 $x_i$ について $x_{i-1}\,R\,x_i$（添字は $n$ を法として読む）なので、$S$ に $R$-極小元がない。$n=1$ の場合が $x\,R\,x$ である。
2．$B$ の空でない部分集合は $A$ の空でない部分集合であり、その $R$-極小元は $R\cap(B\times B)$-極小元でもある。
3．$S$ の $R$-極小元 $m$ について、$y\,R'\,m$ となる $y\in S$ があれば $y\,R\,m$ となり矛盾する。よって $m$ は $R'$-極小元でもある。$\square$

(a) $\Rightarrow$ (b)：$P$ が (b) の仮定を満たすのに $P\neq A$ だとする。$A\setminus P$ は空でないので $R$-極小元 $x$ をもつ。$y\,R\,x$ なら極小性から $y\notin A\setminus P$、すなわち $y\in P$ なので $\operatorname{pred}_R(x)\subset P$ である。仮定から $x\in P$ となり、$x\in A\setminus P$ に反する。
(b) $\Rightarrow$ (a)：空でない $S\subset A$ が $R$-極小元をもたないとし、$P:=A\setminus S$ とおく。$x\in A$ が $\operatorname{pred}_R(x)\subset P$ を満たすとする。もし $x\in S$ なら、$x$ は $S$ の $R$-極小元でないので $y\,R\,x$ となる $y\in S$ があり、$y\in\operatorname{pred}_R(x)\subset P$ に反する。よって $x\in P$ である。(b) により $P=A$、すなわち $S=\emptyset$ となり、仮定に反する。$\square$

$R$-極小元をもたない空でない $S\subset A$ があるとして、無限下降列を作る。$x_0$ を $S$ の $\lhd$-最小元とし、$x_n\in S$ が決まったら、$x_{n+1}$ を $\{y\in S\mid y\,R\,x_n\}$ の $\lhd$-最小元とする。この集合は $x_n$ が $S$ の $R$-極小元でないことから空でない。各段階の選び方が「$\lhd$-最小元」と一通りに決まっているので、列は自然数上の再帰（帰納的定義）で定まり、選択公理は要らない。この列は $x_{n+1}\,R\,x_n$ を満たす。$\square$

$C\subset A$ が 下に閉じている とは、$x\in C$ かつ $y\,R\,x$ なら $y\in C$ となることとする。下に閉じた $C$ を定義域とする関数 $\sigma$ が、すべての $x\in C$ で $\sigma(x)=\mathbf{G}(x,\sigma|_{\operatorname{pred}_R(x)})$ を満たすとき、$\sigma$ を $C$ 上の近似 と呼ぶ（$C$ が下に閉じているので $\operatorname{pred}_R(x)\subset C$ である）。
一致。 $\sigma,\sigma'$ をそれぞれ $C,C'$ 上の近似とすると、$C\cap C'$ 上で $\sigma=\sigma'$ である。実際、$D:=\{x\in C\cap C'\mid\sigma(x)\neq\sigma'(x)\}$ が空でないとし、その $R$-極小元 $x$ をとる。$C\cap C'$ は下に閉じているので $\operatorname{pred}_R(x)\subset C\cap C'$ であり、極小性から $\operatorname{pred}_R(x)$ 上で $\sigma=\sigma'$ である。よって $\sigma(x)=\mathbf{G}(x,\sigma|_{\operatorname{pred}_R(x)})=\mathbf{G}(x,\sigma'|_{\operatorname{pred}_R(x)})=\sigma'(x)$ となり、$x\in D$ に反する。特に、各 $C$ 上の近似は高々一つである。
存在。 近似をもつ下に閉じた部分集合の全体を $\mathcal{D}\subset\mathcal{P}(A)$ とする（分出公理）。$C\in\mathcal{D}$ に $C$ 上のただ一つの近似 $\sigma_C$ を対応させ、置換公理で集合 $\{\sigma_C\mid C\in\mathcal{D}\}$ を作って、その合併を $F$ とおく。一致の主張から $F$ は関数で、その定義域 $D^*:=\bigcup\mathcal{D}$ は下に閉じている。$x\in C\in\mathcal{D}$ なら $F|_C=\sigma_C$ かつ $\operatorname{pred}_R(x)\subset C$ なので、$F(x)=\sigma_C(x)=\mathbf{G}(x,F|_{\operatorname{pred}_R(x)})$ であり、$F$ は $D^*$ 上の近似である。
$D^*\neq A$ とし、$A\setminus D^*$ の $R$-極小元 $x$ をとる。$\operatorname{pred}_R(x)\subset D^*$ なので $C:=D^*\cup\{x\}$ は下に閉じている。$F$ に対 $\bigl(x,\mathbf{G}(x,F|_{\operatorname{pred}_R(x)})\bigr)$ を加えた関数は $C$ 上の近似なので $C\in\mathcal{D}$、よって $x\in D^*$ となり矛盾する。したがって $D^*=A$ であり、$F$ が求める関数である。一意性は一致の主張から従う。$\square$

(b) $\Rightarrow$ (a)：空でない $S\subset A$ について、順序数の空でない集合 $f[S]$ の最小元を $f(m)$（$m\in S$）とする。$y\in S$ が $y\,R\,m$ を満たせば $f(y)< f(m)$ となり最小性に反するので、$m$ は $S$ の $R$-極小元である。
(a) $\Rightarrow$ (b)：$y\,R\,x$ なら $\rho_R(y)+1$ は $\rho_R(x)$ を定める上限の中の一つなので、$\rho_R(y)<\rho_R(y)+1\leq\rho_R(x)$ である。よって $f=\rho_R$ が (b) を満たす。
最小性：(b) の $f$ について、$\rho_R(x)\leq f(x)$ を整礎帰納法で示す。$y\,R\,x$ となるすべての $y$ で $\rho_R(y)\leq f(y)$ なら、$\rho_R(y)+1\leq f(y)+1\leq f(x)$ なので、上限をとって $\rho_R(x)\leq f(x)$ である。
像：$\rho_R[A]$ が下に閉じていること、すなわち $\beta<\rho_R(x)$ なら $\beta\in\rho_R[A]$ を、$x$ についての整礎帰納法で示す。$\beta<\sup\{\rho_R(y)+1\mid y\,R\,x\}$ なら $\beta<\rho_R(y)+1$、すなわち $\beta\leq\rho_R(y)$ となる $y\,R\,x$ がある。$\beta=\rho_R(y)$ ならよく、$\beta<\rho_R(y)$ なら帰納法の仮定による。下に閉じた順序数の集合は順序数である（推移的集合の命題「順序数の集合が順序数になる条件」）。$\square$

1．$f:=\rho_R\circ g$ は $y\,S\,x$ なら $f(y)< f(x)$ を満たすので、thm-wfr-rank により $S$ は整礎である。
2．$y\,R^+\,x$ なら、$\rho_R(z_0)<\rho_R(z_1)<\cdots<\rho_R(z_k)$ から $\rho_R(y)<\rho_R(x)$ である。thm-wfr-rank により $R^+$ は整礎である。
3．空でない $X\subset A\times B$ をとる。第 1 成分の集合 $\{a\mid(a,b)\in X\}$ の $R$-極小元 $a_0$ をとり、$\{b\mid(a_0,b)\in X\}$ の $S$-極小元 $b_0$ をとる。$(a',b')\in X$ が $(a',b')\mathrel{T}(a_0,b_0)$ を満たすとすると、$a_0$ の極小性から $a'\,R\,a_0$ ではないので $a'=a_0$ かつ $b'\,S\,b_0$ となり、$b_0$ の極小性に反する。よって $(a_0,b_0)$ は $T$-極小元である。$\square$