1 集合

集合は現代の抽象数学の基礎概念と言えます。
特にsc_supというoptionが有効です。
それは「集合」と「クラス」を同一視して（いるように）扱えるようにします。
所属関係は2種類あります。「(集合に)属する」と「(クラスに)属する」です。
\(\mathbb{W}\)(ss,p) … \(\in\)

集合は自然にクラスと見なされます。Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
次の自明な定理が生まれます。
\(X = \{ x \mid x \in X \}\) \(\blacktriangleleft\) O
\(X \in Y \Longleftrightarrow X \in Y\) \(\blacktriangleleft\) O

（通常の数学の教科書とは逆に）\(=\) の定義を \(=\) の定義から誘導するのが自然です。
=. … \(X = Y \Longleftrightarrow X = Y\)
この\(\Longleftarrow\)は外延性公理と呼ばれ、ZFの公理の１つです。

クラスが集合となるか、が議論されます。
\(\mathbb{W}_+\)(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

2 集合・クラスの最初の例

宇宙を作ります。
\(\mathbb{W}_+\)(,c) … \(\mathbb{V}\)
\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O

空集合を作ります。
\(\mathbb{W}\)(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\mathbb{W}.\) はbook内変数で「〇. (〇は\(\mathbb{W}\)) という形のpropすべての列」です。この段階では =. ∅. です。
\({\tt P}\) ◀ \(\mathbb{W}.\) は「定義から\({\tt P}\)が示される」と読まれます。
ZFの公理の1つに空集合公理があります。私たちのシステムでは ∅. から導出するのが標準です。
\(\dot\exists \{ x \mid {\perp} \}\) \(\blacktriangleleft\) ∅.

集合でないクラスは固有クラスと呼ばれます。最初の例はRusselクラスです。
\(\mathbb{W}_+\)(,c) … \(\mathbb{V}_0\)
\V0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O

3 包含関係

ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。
\(\mathbb{W}_+\)(cc,p) … \(\subset\)
\(\mathbb{W}\)(ss,p) … \(\subset\)
⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
⊂. … \(X \subset Y \Longleftrightarrow X \subset Y\)
\(\subset\)の定義は\(\subset\)の定義から誘導されます。
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

集合の部分クラスは集合である、ことが要請されます。
ax_s0 … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)

宇宙も固有クラスになります。
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s0

4 ZF

集合論の公理系についてはZF(Zermelo-Fraenkel)が有名です。ZFの中の一つに外延性公理があります。
私たちのシステムではZFの公理そのものを採用せず、wordの定義を作ってZF公理を定理とすることが多いです。