対称モデル

1：$\check x=\{(\check y,\mathbf 1)\mid y\in x\}$ と $\pi\mathbf 1=\mathbf 1$ から、$y$ についての帰納法で従う。後半も階数についての帰納法である。
2：$\pi$ は順序同型なので、$\pi[G]$ は空でなく、弱い条件へ閉じ、二元が $\pi[G]$ の中に共通の強化をもつ。$D\in M$ が稠密なら $\pi^{-1}[D]\in M$ も稠密なので $G$ と交わり、$D$ は $\pi[G]$ と交わる。$\pi\in M\subset M[G]$ なので $\pi[G]\in M[G]$ であり、ジェネリック拡大 の定理「ジェネリック拡大の最小性」により $M[\pi[G]\,]\subset M[G]$ である。$G=\pi^{-1}[\pi[G]\,]$ に同じ議論を当てて逆の包含を得る。
3：$\tau$ の階数についての帰納法で、
$$ (\pi\tau)^{\pi[G]}=\{(\pi\sigma)^{\pi[G]}\mid(\sigma,p)\in\tau,\ \pi p\in\pi[G]\}=\{\sigma^G\mid(\sigma,p)\in\tau,\ p\in G\}=\tau^G $$
である。$\square$

$p\Vdash\varphi(\vec\tau)$ とし、$H$ を $\pi p\in H$ となる $M$ 上ジェネリックなフィルターとする。$G:=\pi^{-1}[H]$ は prop-symmetric-model-automorphism の 2 によりジェネリックで、$p\in G$ を満たす。よって $M[G]\models\varphi(\vec\tau^G)$ である。同じ命題の 2・3 により $M[H]=M[G]$、$(\pi\tau_i)^H=\tau_i^G$ なので、$M[H]\models\varphi((\pi\tau_1)^H,\dots,(\pi\tau_k)^H)$ である。$H$ は任意なので $\pi p\Vdash\varphi(\pi\vec\tau)$ である。逆向きは $\pi^{-1}$ に同じ議論を当てればよい。$\square$

1：$\rho\tau=\tau$ なら $(\pi\rho\pi^{-1})(\pi\tau)=\pi\rho\tau=\pi\tau$ であり、逆も同様なので等式が成り立つ。正規フィルターの条件 3 により、$\tau$ が対称なら $\pi\tau$ も対称である。$\pi\tau$ の対の第一成分は $\pi\sigma$（$\sigma$ は $\tau$ の対の第一成分）なので、階数についての帰納法で $\pi\tau\in\mathrm{HS}$ が従う。
2：$\mathcal F$ は空でなく条件 1 を満たすので $\mathcal G\in\mathcal F$ である。prop-symmetric-model-automorphism の 1 により $\operatorname{sym}(\check x)=\mathcal G$ であり、$\check x$ の対の第一成分も標準名なので、帰納法で $\check x\in\mathrm{HS}$ である。
3：$y\in\tau^G$（$\tau\in\mathrm{HS}$）なら、ある $(\sigma,p)\in\tau$ について $p\in G$、$y=\sigma^G$ であり、$\sigma\in\mathrm{HS}$ なので $y\in N$ である。2 と $\check x^G=x$ から $M\subset N$ であり、$N\subset M[G]$ は定義から明らかである。$\square$

1：$\hat\pi\check k=\check k$ であり、$q=\hat\pi p$ が $P$ 全体を動くとき $q(\pi(n),k)=p(n,k)$ なので、$\hat\pi\dot a_n=\{(\check k,q)\mid q(\pi(n),k)=1\}=\dot a_{\pi(n)}$ である。よって $\operatorname{sym}(\dot a_n)\supset\operatorname{fix}(\{n\})\in\mathcal F$ であり、対の第一成分 $\check k$ は $\mathrm{HS}$ に属するので $\dot a_n\in\mathrm{HS}$ である。$\hat\pi\dot A=\{(\dot a_{\pi(n)},\mathbf 1)\}=\dot A$ なので $\operatorname{sym}(\dot A)=\mathcal G$ であり、$\dot A\in\mathrm{HS}$ である。
2：$D=\{p\mid(\exists k)\ (n,k),(m,k)\in\operatorname{dom}p,\ p(n,k)\ne p(m,k)\}\in M$ は稠密である（$p$ の定義域に現れない $k$ を選び、$(n,k)$ に $1$、$(m,k)$ に $0$ を置けばよい）。任意のジェネリックな $G$ は $D$ の元 $p$ を含む。$p(n,k)=1$、$p(m,k)=0$ なら $k\in a_n$ であり、$k\in a_m$ とすると、$q(m,k)=1$ となる $q\in G$ があり、$q$ と $p$ が両立しなくなって、$G$ の二元が両立することに反する。よって $k\notin a_m$ である。逆の値でも同様なので $a_n\ne a_m$ である。よって $A$ は $M[G]$ で無限であり、$N\subset M[G]$ なので、$N$ の中の $A$ から自然数への全単射もなく、$A$ は $N$ でも無限である。$\square$

単射 $f\colon\omega\to A$ が $N$ に属するとし、$f=\tau^G$（$\tau\in\mathrm{HS}$）とする。「$f$ は $\omega$ から $A$ への単射である」は推移的なクラスの間で真偽が変わらない言明なので、$M[G]$ でも成り立つ。強制定理により、ある $p_0\in G$ が「$\tau$ は $\check\omega$ から $\dot A$ への単射である」を強制する。
$\tau$ は対称なので、ある有限集合 $E\subset\omega$ について $\operatorname{fix}(E)\subset\operatorname{sym}(\tau)$ である。prop-symmetric-model-cohen-set の 2 により $\{a_n\mid n\in E\}$ はちょうど $|E|$ 個の元からなり、$f(0),\dots,f(|E|)$ は相異なるので、ある $i$ とある $n\notin E$ について $f(i)=a_n$ である。強制定理により、$p\Vdash\tau(\check i)=\dot a_n$ となる $p\in G$ があり、$G$ の中で $p_0$ と共通の強化をとって $p\le p_0$ としてよい。
$p$ の定義域は有限なので、$n'\notin E\cup\{n\}$ で、$(n',k)\in\operatorname{dom}p$ となる $k$ がないものを選べる。$\pi$ を $n$ と $n'$ を入れ替える互換とする。$\hat\pi\in\operatorname{fix}(E)\subset\operatorname{sym}(\tau)$ なので $\hat\pi\tau=\tau$ であり、$\hat\pi\check i=\check i$、$\hat\pi\dot a_n=\dot a_{n'}$ である。thm-symmetric-model-symmetry-lemma により
$$ \hat\pi p\Vdash\tau(\check i)=\dot a_{n'} $$
である。$p$ と $\hat\pi p$ は両立する。実際、第 $n$ 行と第 $n'$ 行以外では $\hat\pi p$ と $p$ は同じ値をとり、$\hat\pi p$ の第 $n$ 行は $p$ の第 $n'$ 行から来るので空である。$\hat\pi p$ の第 $n'$ 行は $p$ の第 $n$ 行から来るが、$p$ の第 $n'$ 行は空である。よって $r=p\cup\hat\pi p$ は条件で、$r\le p$、$r\le\hat\pi p$ である。
$r$ を含むジェネリックな $H$ をとると（ジェネリックフィルター の系「可算推移モデル上の存在」）、$r\le p\le p_0$ なので $M[H]$ で $\tau^H$ は関数であり、$p,\hat\pi p\in H$ から $\dot a_n^H=\tau^H(i)=\dot a_{n'}^H$ となる。これは $n\ne n'$ と prop-symmetric-model-cohen-set の 2 に反する。$\square$

$N$ が ZF のモデルであることは thm-symmetric-model-zf による。ZF の中で、整列できる無限集合 $X$ には単射 $\omega\to X$ がある（整列順序の最初の $\omega$ 個の元をとる）。thm-symmetric-model-dedekind-finite により、$N$ で $A$ は整列できない。$A\subset\mathcal P(\omega)$ なので、$\mathcal P(\omega)$ も $N$ で整列できない。ZF のもとで選択公理は整列可能定理と同値なので（選択公理、整列可能定理）、$N$ では選択公理が成り立たない。$\square$