Morse–Kelley集合論

1. $D=\{m\in\omega\mid m\le n\to\forall\varphi\in\mathrm{Fml}_{\le m}\ \forall s\ (\langle\varphi,s\rangle\in X\leftrightarrow\langle\varphi,s\rangle\in X')\}$ は述語的な内包で得られるクラスと $\omega$ の共通部分なので集合である。$0\in D$ は (T1)(T2) の右辺が $X,X'$ によらないことによる。$m\in D$、$m+1\le n$ とし、$c(\varphi)=m+1$ とすると、$\varphi$ は $\lnot\psi$、$\psi\to\chi$、$\forall v_i\,\psi$ のどれかで $c(\psi),c(\chi)\le m$ なので、(T3)〜(T5) により $X$ と $X'$ で同じ条件で決まる。よって $m+1\in D$ で、帰納法により $D=\omega$。$m=n$ から $X=X'$ である。
2. (T1)〜(T5) の右辺には、左辺の論理式の真部分論理式（$c$ がより小さい）しか現れないことによる。
3. $X'=X\cup\{\langle\varphi,s\rangle\mid c(\varphi)=n+1,\ s\in\mathrm{Asg},\ \varphi\text{ の形に応じた (T3)〜(T5) の右辺が }X\text{ について成り立つ}\}$ とおく。右辺の量化は集合 $y$ だけなので、述語的な内包でクラスとして得られ、$\mathrm{Tar}(X',n+1)$ を満たす。$\mathrm{Tar}(X,0)$ の $X$ は (T1)(T2) の右辺で定まる原子論理式の部分として同様に得られる。$\square$

$S=\{n\in\omega\mid\exists X\ \mathrm{Tar}(X,n)\}$ とおく。条件は「あるクラス $X$ が存在する」というクラスの量化を含むので、ここで MK の内包 (e') を使い、分出 (c) により $S$ は集合である。lem-mk-partial の 3 により $0\in S$ で、$n\in S$ なら $n+1\in S$ なので、帰納法により $S=\omega$ である。次に、再び (e') により
$$ T=\bigl\{\langle\varphi,s\rangle\ \big|\ \exists n\in\omega\ \exists X\ \bigl(\mathrm{Tar}(X,n)\land\langle\varphi,s\rangle\in X\bigr)\bigr\} $$
とおく。$c(\varphi)\le n$ で $\mathrm{Tar}(X_n,n)$ なら、$\langle\varphi,s\rangle\in T\leftrightarrow\langle\varphi,s\rangle\in X_n$ である。実際、$\mathrm{Tar}(X',m)$ で $\langle\varphi,s\rangle\in X'$ なら、$k=\min(m,n)$ として lem-mk-partial の 2 で $X'$ と $X_n$ を $\mathrm{Fml}_{\le k}$ に制限すると、1 によりそれらは一致する。各論理式 $\varphi$ について $\mathrm{Tar}(X_n,n)$ となる $X_n$（$n=c(\varphi)$）がとれるので、$T$ は (T1)〜(T5) を満たす。一意性は lem-mk-partial の 1 と同じ帰納法による。$\square$

MK の中で議論し、thm-mk-truth の真理のクラス $T$ を固定する。以下で使う内包はすべて $T$ をパラメータとする述語的なものである。
段 1（ZFC の公理は $T$ で妥当）．外延性・基礎・対・合併・冪集合・無限・選択の各公理 $\sigma$ は一つの文である。各論理式 $\varphi(v_0,\dots,v_{k-1})$ について $\langle\ulcorner\varphi\urcorner,s\rangle\in T\leftrightarrow\varphi(s(0),\dots,s(k-1))$ であることが、$\varphi$ の組み立てについての帰納法（(T1)〜(T5) を順にたどる）で分かるので、MK の公理 (b) により $\sigma$ は $T$ で妥当である。分出図式と置換図式の例は無限個あり、MK の中の符号 $\varphi$ すべてについて一様に示す必要がある。分出の例では、割り当て $s$ と集合 $a$ に対し、$A=\{x\mid\langle\varphi,s(i/x)\rangle\in T\}$ はクラスで、(c) により $b=A\cap a$ は集合であり、これが例の結論の $b$ になる。置換の例では、仮定が $T$ で真ならクラス $F=\{\langle x,y\rangle\mid x\in a,\ \langle\varphi,s(i/x)(j/y)\rangle\in T\}$ が関数になり、(d) により像 $F[a]$ が集合で、これが結論の $b$ になる。

$\mathfrak K$ のクラスは $V_\kappa$ の部分集合である。$x\in V_\kappa$ なら $x\in V_\kappa\in V_{\kappa+1}$ なので $x$ は集合であり、逆に $x\in Y\in V_{\kappa+1}$ なら $x\in Y\subseteq V_\kappa$ である。よって集合の全体は $V_\kappa$ で、集合どうしの所属は本当の $\in$ である。$V_\kappa$ は推移的なので、集合の順序対は $\mathfrak K$ の中でも本当の順序対である。
(a)：$X,Y\subseteq V_\kappa$ の $\mathfrak K$ での元は本当の元なので、同じ元をもてば $X=Y$。(b)：$(V_\kappa,\in)\models\mathsf{ZFC}$（到達不能基数 の定理「到達不能基数からZFCの集合モデルが得られる」）であり、集合の量化は $V_\kappa$ を動く。(c)：$a\in V_\kappa$ なら $a\subseteq V_\alpha$（$\alpha<\kappa$）なので $X\cap a\subseteq V_\alpha$、すなわち $X\cap a\in V_{\alpha+1}\subseteq V_\kappa$。(d)：$F\subseteq V_\kappa$ が関数、$a\in V_\kappa$ とする。$\lvert F[a]\rvert\le\lvert a\rvert<\kappa$（到達不能基数 の命題「階層の各段は小さい」）であり、$F[a]$ の各元の階数は $\kappa$ 未満なので、$\kappa$ の正則性によりそれらの上限 $\beta$ も $\kappa$ 未満で、$F[a]\subseteq V_{\beta+1}$、$F[a]\in V_{\beta+2}\subseteq V_\kappa$ である。
(e')：論理式 $\varphi(y,\vec P)$ と $\vec P\in V_{\kappa+1}$ をとる。$\mathfrak K$ は集合の構造なので、充足関係 $\mathfrak K\models\varphi[\cdots]$ は ZFC の中で定義されている（Tarskiの真理定義 の定理「Tarski の条件を満たす写像の存在と一意性」）。分出により $D=\{y\in V_\kappa\mid\mathfrak K\models\varphi[y,\vec P]\}$ は $V_\kappa$ の部分集合であり、$V_{\kappa+1}=\mathcal P(V_\kappa)$ に属する。$\varphi$ がクラスを量化していても $D$ は $\mathfrak K$ のクラスで、$\mathfrak K$ の中で $\forall y\,(y\in D\leftrightarrow\varphi(y,\vec P))$ が成り立つ。$\square$

thm-mk-inaccessible により、到達不能基数 $\kappa$ に対し $\mathfrak K$ は MK の公理をすべて満たす集合の構造である。ZFC の中で健全性定理（一階述語論理の証明体系 の定理「健全性定理」）を $\mathfrak K$ に使うと、MK から $\psi$ と $\lnot\psi$ の両方が導出されることはない。$\square$