5 集合の存在について①

5.1 クラスが集合となるか

word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

集合でないクラスは固有クラスと呼ばれます。最初の例はRussellクラスです。
word(,c) … \(\mathbb{V}_0\)
𝕍0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
¬Exi𝕍0 … \(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O
　ソース：prop/thm ¬Exi𝕍0 <- `¬ Exi 𝕍0` ◀ O　prf ¬Exi𝕍0 -| O p;

もう一つ例を作ってみます。
word(,c) … \(\mathbb{V}_1\)
𝕍1. … \(\mathbb{V}_1 = \{ x \mid \not\exists y \, ( x \in y \in x ) \}\)
¬Exi𝕍1 … \(\neg \dot\exists \mathbb{V}_1\) \(\blacktriangleleft\) O
　ソース：prop/thm ¬Exi𝕍1 <- `¬ Exi 𝕍1` ◀ O　prf ¬Exi𝕍1 -| O p;
𝕍1⊂_𝕍0 … \(\mathbb{V}_1 \subset \mathbb{V}_0\) \(\blacktriangleleft\) O
　ソース：prop/thm 𝕍1⊂_𝕍0 <- `𝕍1 ⊂_ 𝕍0` ◀ O　prf 𝕍1⊂_𝕍0 -| O p;
𝕍1=_cls … \(\mathbb{V}_1 = \{ x \mid x \notin \bigcup x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm 𝕍1=_cls <- `𝕍1 =_ \{ cls x | x {/}∈ ⋃ x \}` ◀ W.　prf 𝕍1=_cls -| ⋃. p; 𝕍1=_cls -| W. h;

5.2 ZF

集合論の公理系についてはZF(Zermelo-Fraenkel)が有名です。
=.の\(\Longleftarrow\) は外延性公理と呼ばれ、ZFの公理の１つです。ZFの公理は、これと正則性公理（5.4）以外は集合の存在を主張するものです。

以下のZFの4公理は、Matheliaではwordの定義から導出される定理とすることが多いです。ただし公理が要らなくなるのではありません：∅・set2・℘・⋃ を返り値が s の語として定義 prop を置いた時点で、その集合が存在することを仮定しています。存在の仮定を、公理から定義 prop へ移したと読みます。
空集合公理
ax_∅ … \(\dot\exists \{ x \mid {\perp} \}\) \(\blacktriangleleft\) ∅.
　ソース：prop/thm ax_∅ <- `Exi \{ cls x | ⊥ \}` ◀ ∅.　prf ax_∅ -| ∅. p;
対集合公理
ax_set2 … \(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.
　ソース：prop/thm ax_set2 <- `Exi \{ cls a | a = x or a = y \}` ◀ set2.　prf ax_set2 -| set2. p;
べき集合公理
ax_℘ … \(\dot\exists \{ A \mid A \subset X \}\) \(\blacktriangleleft\) ℘.
　ソース：prop/thm ax_℘ <- `Exi \{ cls A | A ⊂ X \}` ◀ ℘.　prf ax_℘ -| ℘. p;
和集合公理
ax_⋃ … \(\dot\exists \{ x \mid \exists X \in \mathcal{X} . x \in X \}\) \(\blacktriangleleft\) ⋃.
　ソース：prop/thm ax_⋃ <- `Exi \{ cls x | [ ∃ X ∈ calX . x ∈ X ] \}` ◀ ⋃.　prf ax_⋃ -| ⋃. p;

5.3 無限公理

後続関数を準備しておきます。von Neumannは自然数を \(0 = \emptyset\) , \(1 = \emptyset \textit{+1}\) , … と作っていきました。
word(s,s) … \(\textit{+1}\)
suc. … \(n \textit{+1} = n \cup \{ n \}\)
先の4公理は初等的な集合を作り出しますが、無限集合は次の公理により初めて生まれます。
ax_∞ … \(\exists M ( \emptyset \in M , \forall x \in M . x \textit{+1} \in M )\)
空集合公理 は 無限公理 から導出されます。ただし下の prf は ∅. も前提に使っているので（ax_∞ の式自体が ∅ を含む）、「無限公理だけから空集合の存在が出る」ことを示す例にはなっていません。
ax_∅ \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_∞
　ソース：thm ax_∅ ◀ W. , ax_∞　prf ax_∅ -| ax_∞ , ∅. p; ax_∅ -| W. , ax_∞ h;

5.4 正則性公理(基礎の公理)

次の公理はvon Neumannによって導入されたものです。
ax0 … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
　ソース：!prop/thm ax0' ◀ W. , ax0　prf ax0' -| ax0 // W. p; ax0' -| W. , ax0 h;
𝕍1=_𝕍 … \(\mathbb{V}_1 = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax0
　ソース：prop/thm 𝕍1=_𝕍 <- `𝕍1 =_ 𝕍` ◀ W. , ax0　prf 𝕍1=_𝕍 / W. -| ax_set2 , ax0' p; 𝕍1=_𝕍 -| W. , ax0 h;