NBG集合論

1. 対の公理により各 $a\in A$ はある $\{a,a\}\in A$ の元なので、$A$ の元はすべて集合である。$P$ の元はどの元にも属さないので集合でない。集合についての論理式の量化は $A$ を動き、所属は $E$ で判定されるので、後半は相対化の補題（公理的集合論 の補題「相対化の補題」）による。
   (a)：$X\mapsto\operatorname{ext}(X)$ は単射である。$A$ の上では $\mathfrak A$ の外延性により単射で、$P$ の元はそれ自身が $\operatorname{ext}$ であり、どの $\operatorname{ext}(a)$ とも異なるからである。
   (e)：述語的な論理式 $\varphi(y,\vec p,\vec Y)$ と、$\vec p\in A$、クラス $\vec Y$ をとる。各 $Y_l$ について $\operatorname{ext}(Y_l)$ は論理式 $\psi_l(x,\vec b_l)$ で定義される。$\varphi$ の原子論理式を次のように書き換えて、集合論の言語の論理式 $\varphi^*$ を作る：$u\in Y_l$ は $\psi_l(u,\vec b_l)$ に、$Y_l\in u$ と $u=Y_l$ は、$Y_l$ が $c\in A$ なら $c\in u$、$u=c$ に、$Y_l\in P$ なら偽な文 $\lnot\, u=u$ に、$Y_l\in Y_{l'}$ と $Y_l=Y_{l'}$ は $\mathcal N(\mathfrak A)$ での真偽に応じて $u=u$ か $\lnot\,u=u$ に（$u$ は任意の変数）。$\varphi$ の量化は集合を動くので $A$ を動き、$b\in A$ について $\mathcal N(\mathfrak A)\models\varphi[b,\vec p,\vec Y]\iff\mathfrak A\models\varphi^*[b,\vec p,\vec b_1,\dots]$ が論理式の組み立てについての帰納法で分かる。右辺を満たす $b$ の全体 $D$ は定義可能なので、$D=\operatorname{ext}(X)$ となる $X\in\mathcal N(\mathfrak A)$（$D$ がある $\operatorname{ext}(c)$ なら $X=c$、そうでなければ $X=D\in P$）があり、これが (e) の $X$ である。
2. (b) は 1 の後半による。(c)：$\operatorname{ext}(X)$ が $\psi(x,\vec b)$ で定義されるとき、$\mathfrak A$ の分出図式から $\operatorname{ext}(c)=\{x\mathrel{E}a\mid\psi(x,\vec b)\}$ となる $c\in A$ があり、$c$ が $X\cap a$ である。(d)：集合の順序対は集合の量化だけで定義されるので、$\mathcal N(\mathfrak A)$ の順序対は $\mathfrak A$ の順序対と一致する。$F$ が関数で、$\operatorname{ext}(F)$ が $\psi(z,\vec b)$ で定義されるとする。$\theta(x,y)$ を「$\psi(\langle x,y\rangle,\vec b)$」とおくと、各 $x$ に対し $\theta(x,y)$ を満たす $y$ は高々一つである。分出図式で $a'=\{x\mathrel{E}a\mid\exists y\,\theta(x,y)\}$ をとると、$a'$ の各元に $\theta$ を満たす $y$ がちょうど一つあるので、置換図式により $y\mathrel{E}b'\leftrightarrow\exists x\mathrel{E}a'\ \theta(x,y)$ となる $b'\in A$ がある。$b'$ が $F[a]$ である。$\square$

$\mathsf{ZFC}\vdash\sigma$ なら $\mathsf{NBG}\vdash\sigma$ であることは上に引いた。逆に $\mathsf{NBG}\vdash\sigma$ とし、$\mathfrak A$ を ZFC の任意のモデルとする。thm-nbg-model により $\mathcal N(\mathfrak A)$ は NBG のモデルなので、健全性により $\mathcal N(\mathfrak A)$ は $\sigma$ の相対化を満たし、同定理の 1 により $\mathfrak A\models\sigma$ である。$\mathfrak A$ は任意なので $\sigma$ は ZFC の論理的帰結であり、Gödelの完全性定理 の定理「Gödelの完全性定理」により $\mathsf{ZFC}\vdash\sigma$ である。
等無矛盾性：$\sigma$ を $\lnot\,\forall x\,(x=x)$ とすると、どちらかが矛盾すれば $\sigma$ を証明し、上の同値によりもう一方も $\sigma$ を証明する。$\square$

結合子は $\lnot,\land$、量化は $\exists$ を基本とし、ほかは略記とみる。$\varphi$ の組み立てについての帰納法で、各場合に $C$ を (G0)〜(G9) と上の操作で作る。各自然数 $k,i,j$ は空集合から対と合併で作れる集合である。
原子論理式：$v_i\in v_j$ なら $C=\mathrm{Sq}_k\cap\mathrm R_\in\langle\langle i,j\rangle\rangle$、$v_i=v_j$ なら $\mathrm R_=$ で同様にする。$v_i\in Y$ なら、$B=\operatorname{dom}\bigl(\mathrm{Ap}\cap(V\times Y)\bigr)=\{\langle s,i'\rangle\mid s(i')\in Y\}$ として $C=\mathrm{Sq}_k\cap B\langle i\rangle$ とする。$Y\in v_i$ は、$Y$ が集合なら $B=\operatorname{dom}\bigl(\mathrm{In}\cap(V\times\{Y\})\bigr)$ として $C=\mathrm{Sq}_k\cap B\langle i\rangle$、$Y$ が集合でなければ $C=\emptyset$ とする。$v_i=Y$ も同様に $\mathrm{Ap}$ を使う（$Y$ が集合でなければ $C=\emptyset$）。クラスの変数だけの原子論理式は、成り立つなら $C=\mathrm{Sq}_k$、成り立たないなら $C=\emptyset$ とする。
結合子：$\lnot\varphi$ には $\mathrm{Sq}_k\setminus C_\varphi$、$\varphi\land\psi$ には $C_\varphi\cap C_\psi$ をとる。
量化：$\varphi=\exists v_i\,\chi$ とする（量化は集合の変数についてのもの）。$k'=\max(k,i+1)$ とおくと、$\chi$ の自由な集合の変数は $v_0,\dots,v_{k'-1}$ の中にあるので、帰納法の仮定から $C'=\{t\in\mathrm{Sq}_{k'}\mid\chi[t]\}$ がある。
$$ C=\mathrm{Sq}_k\cap\operatorname{dom}\bigl(\mathrm{Ag}\cap(V\times(C'\times\{i\}))\bigr) $$
とおく。$s\in C$ なら、$\chi[t]$ を満たす $t\in\mathrm{Sq}_{k'}$ で $j\neq i$ の位置が $s$ と一致するものがあり、$\chi$ の自由変数は $v_i$ と $\varphi$ の自由変数なので、$v_i$ に $t(i)$ を代入すれば $\chi$ が成り立つ。すなわち $\varphi[s]$ である。逆に $\varphi[s]$ なら、$\chi$ を満たす $v_i$ の値 $y$ をとり、$t$ を「$j< k$、$j\neq i$ では $s(j)$、$i$ では $y$、そのほかは $\emptyset$」とすれば、$t$ は対と合併で作れる長さ $k'$ の列で $t\in C'$、$\langle s,\langle t,i\rangle\rangle\in\mathrm{Ag}$ なので $s\in C$ である。$\square$

(G0)〜(G9) は (e) の例なので NBG の定理であり、$\mathsf{NBG}_0$ の定理は NBG の定理である。逆を示す。(e) の例 $\forall\vec p\,\forall\vec Y\,\exists X\,\forall y\,(y\in X\leftrightarrow\varphi(y,p_1,\dots,p_n,\vec Y))$ をとる。束縛変数を付け替えて、$y=v_0$、$p_j=v_j$（$1\le j\le n$）とし、$k=n+1$ とする。lem-nbg-sequences で $C=\{s\in\mathrm{Sq}_k\mid\varphi[s]\}$ をとる。集合 $p_1,\dots,p_n$ を固定し、$B_j=\operatorname{dom}\bigl(\mathrm{Ap}\cap(V\times\{p_j\})\bigr)\langle j\rangle=\{s\mid s(j)=p_j\}$、$C^\circ=C\cap B_1\cap\dots\cap B_n$ とおき、
$$ X=\operatorname{dom}\Bigl(\bigl(\mathrm{Ap}\cap((C^\circ\times\{0\})\times V)\bigr)^{-1}\Bigr)=\{y\mid\exists s\in C^\circ\ y=s(0)\} $$
とする。$y\in X$ なら $\varphi(y,\vec p,\vec Y)$ である。逆に $\varphi(y,\vec p,\vec Y)$ なら、列 $s=\{\langle0,y\rangle,\langle1,p_1\rangle,\dots,\langle n,p_n\rangle\}$ が $C^\circ$ に属し、$y=s(0)\in X$ である。$\square$