空 そら 集合 しゅうごう 必 かなら 自分 じぶん 自身 じしん 交 まじ 要素 ようそ 持 も
∀
A
(
A
≠
∅
⟹
∃
x
∈
A
,
∀
t
∈
A
(
t
∉
x
)
)
{\displaystyle \forall A{\bigl (}A\neq \varnothing \implies \exists x\in A,\forall t\in A(t\notin x){\bigr )}}
以下 いか 主張 しゅちょう ZF公理系 こうりけい の他 ほか 公理 こうり 元 もと 同値 どうち 正則 せいそく 性 せい 公理 こうり 採用 さいよう 差 さ 支 つか [1]
ここで、V は集合 しゅうごう 論 ろん 宇宙 うちゅう 指 さ WF は整 せい 礎 いしずえ 的 てき 集合 しゅうごう 全体 ぜんたい クラス （フォン・ノイマン宇宙 うちゅう ）を指 さ
ZF公理系 こうりけい 内 ない 限 かぎ 話 はなし 進 すす 各 かく 順序 じゅんじょ 数 すう α あるふぁ 対 たい R (α あるふぁ 次 つぎ 定義 ていぎ
P
{\displaystyle {\mathcal {P}}}
冪 べき 集合 しゅうごう
R
(
0
)
=
∅
{\displaystyle R(0)=\varnothing }
R
(
α あるふぁ +
1
)
=
P
(
R
(
α あるふぁ )
)
{\displaystyle R(\alpha +1)={\mathcal {P}}(R(\alpha ))}
α あるふぁ 極限 きょくげん 順序 じゅんじょ 数 すう
R
(
α あるふぁ )
=
⋃
β べーた <
α あるふぁ
R
(
β べーた )
{\displaystyle R(\alpha )=\bigcup _{\beta <\alpha }R(\beta )}
クラス WF はこれらを全 すべ 集 あつ 定義 ていぎ
W
F
=
⋃
α あるふぁ ∈
O
N
R
(
α あるふぁ )
{\displaystyle {\mathit {WF}}=\bigcup _{\alpha \in {\mathit {ON}}}R(\alpha )}
ZF公理系 こうりけい 他 ほか 公理 こうり 得 え 種々 しゅじゅ 集合 しゅうごう 演算 えんざん 対 たい 集合 しゅうごう 和 わ 集合 しゅうごう 冪 べき 集合 しゅうごう 結果 けっか 集合 しゅうごう 常 つね WF 内 うち 含 ふく V = WF 仮定 かてい 全 すべ 集合 しゅうごう ∅ に通常 つうじょう 集合 しゅうごう 演算 えんざん 施 ほどこ 得 え 制限 せいげん 主張 しゅちょう 例 たと x = {x }集合 しゅうごう x ∈ y y ∈ x 集合 しゅうごう 正則 せいそく 性 せい 公理 こうり 下 した 集合 しゅうごう 得 え
定理 ていり ―
任意 にんい α あるふぁ ON 対 たい
R
(
α あるふぁ )
{\displaystyle R(\alpha )}
推移 すいい 的 てき
∀
β べーた ≤
α あるふぁ ;
R
(
β べーた )
⊆
R
(
α あるふぁ )
{\displaystyle \forall \beta \leq \alpha ;R(\beta )\subseteq R(\alpha )}
証明 しょうめい 超 ちょう 限 きり 帰納 きのう 法 ほう α あるふぁ 明 あき ∀β べーた α あるふぁ に対 たい 成 な 立 た 仮定 かてい α あるふぁ β べーた 仮定 かてい R (β べーた 推移 すいい 的 てき
R
(
α あるふぁ )
=
P
(
R
(
β べーた )
)
{\displaystyle R(\alpha )={\mathcal {P}}(R(\beta ))}
推移 すいい 的 てき
R
(
β べーた )
⊂
P
(
R
(
β べーた )
)
=
R
(
α あるふぁ )
{\displaystyle R(\beta )\subset {\mathcal {P}}(R(\beta ))=R(\alpha )}
α あるふぁ 極限 きょくげん 順序 じゅんじょ 数 すう 仮定 かてい ∀β べーた α あるふぁ に対 たい R (β べーた 推移 すいい 的 てき 推移 すいい 的 てき 集合 しゅうごう 和 わ 集合 しゅうごう 推移 すいい 的 てき
R
(
α あるふぁ )
=
⋃
β べーた <
α あるふぁ
R
(
β べーた )
{\displaystyle R(\alpha )=\bigcup _{\beta <\alpha }R(\beta )}
も推移 すいい 的 てき
∀
β べーた <
α あるふぁ ;
R
(
β べーた )
⊂
⋃
β べーた <
α あるふぁ
R
(
β べーた )
=
R
(
α あるふぁ )
{\displaystyle \forall \beta <\alpha ;R(\beta )\subset \bigcup _{\beta <\alpha }R(\beta )=R(\alpha )}
も同様 どうよう
WF の定義 ていぎ x ∈ WF x ∈ R (α あるふぁ 満 み 最小 さいしょう 順序 じゅんじょ 数 すう α あるふぁ 後続 こうぞく 順序 じゅんじょ 数 すう 実際 じっさい α あるふぁ 極限 きょくげん 順序 じゅんじょ 数 すう x ∈ R (α あるふぁ 及 およ ∀β べーた α あるふぁ x ∉ R (β べーた が成 な 立 た
x
∉
⋃
β べーた <
α あるふぁ
R
(
β べーた )
=
R
(
α あるふぁ )
{\displaystyle x\notin \bigcup _{\beta <\alpha }R(\beta )=R(\alpha )}
となって矛盾 むじゅん
そこで、集合 しゅうごう x のランクを次 つぎ 定義 ていぎ
x ∈ WF x ∈ R (β べーた 満 み 最小 さいしょう β べーた 集合 しゅうごう x のランクといい、rank(x ) で表 あらわ
よって、rank(x ) = β べーた ならば
∀
α あるふぁ >
β べーた ;
x
∈
R
(
α あるふぁ )
{\displaystyle \forall \alpha >\beta ;x\in R(\alpha )}
が成 な 立 た x ∈ R (β べーた x ⊂ R (β べーた 概念 がいねん 用 もち R (α あるふぁ 次 つぎ 特徴付 とくちょうづ
∀
α あるふぁ ;
R
(
α あるふぁ )
=
{
x
∈
W
F
∣
rank
(
x
)
<
α あるふぁ }
{\displaystyle \forall \alpha ;R(\alpha )=\{x\in {\mathit {WF}}\mid \operatorname {rank} (x)<\alpha \}}
及 およ
∀
x
∈
W
F
(
rank
(
x
)
<
α あるふぁ ⟺
∃
β べーた <
α あるふぁ ;
x
∈
R
(
β べーた +
1
)
⟺
x
∈
R
(
α あるふぁ )
)
{\displaystyle \forall x\in {\mathit {WF}}{\bigl (}\operatorname {rank} (x)<\alpha \iff \exists \beta <\alpha ;x\in R(\beta +1)\iff x\in R(\alpha ){\bigr )}}
ランクを計算 けいさん 次 つぎ 補題 ほだい 使 つか
y
∈
W
F
{\displaystyle y\in {\mathit {WF}}}
x
∈
y
⟹
x
∈
W
F
{\displaystyle x\in y\implies x\in {\mathit {WF}}}
かつ
rank
(
x
)
<
rank
(
y
)
{\displaystyle \operatorname {rank} (x)<\operatorname {rank} (y)}
rank
(
y
)
=
α あるふぁ
{\displaystyle \operatorname {rank} (y)=\alpha }
y
∈
R
(
α あるふぁ +
1
)
=
P
(
R
(
α あるふぁ )
)
{\displaystyle y\in R(\alpha +1)={\mathcal {P}}(R(\alpha ))}
x
∈
y
{\displaystyle x\in y}
x
∈
R
(
α あるふぁ )
=
{
x
∈
W
F
∣
rank
(
x
)
<
α あるふぁ }
{\displaystyle x\in R(\alpha )=\{x\in {\mathit {WF}}\mid \operatorname {rank} (x)<\alpha \}}
rank
(
x
)
<
α あるふぁ
{\displaystyle \operatorname {rank} (x)<\alpha }
