1 集合・クラスの基本

1.1 準備：book4で紹介されたもの

word(sc,p) … \(\in\)
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

1.2 所属関係、等号

集合は現代の抽象数学の基礎概念と言え、その公理系についてはZF(Zermelo-Fraenkel)が有名です。
MatheliaはZF公理系も容易に記述し、数学のスタートをスムーズにします。
所属関係は2種類になります。「(クラスに)属する」以外に「(集合に)属する」が出てきます。
word(ss,p) … \(\in\)

集合とクラスを同一視して（いるように）扱えます。
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は Formel によって \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
次の自明に見える定理が生まれます。
\(X \in Y \Longleftrightarrow X \in Y\) \(\blacktriangleleft\) O
\(X = \{ x \mid x \in X \}\) \(\blacktriangleleft\) O

（通常の数学の教科書とは逆に）\(=\) の定義は \(=\)の定義から誘導するのが自然です。
=. … \(X = Y \Longleftrightarrow X = Y\)
=.|cvt … \(X = Y \Longleftrightarrow \forall x ( x \in X \Longleftrightarrow x \in Y )\) 　です。この \(\Longleftarrow\) は「外延性公理」です（ZF公理の１つ）。

1.3 包含関係

ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。
word(cc,p) … \(\subset\)
word(ss,p) … \(\subset\)
⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
⊂. … \(X \subset Y \Longleftrightarrow X \subset Y\)

\({\tt A}\) / \({\tt P}\) は「\({\tt A}\)|cvt を \({\tt P}\)|cvt で展開したもの」です。ソース39行目で / W. が使われています。ここでは \(\mathbb{W}.\) は =. と ⊂. です。
\(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.4 宇宙、空集合

word(,c) … \(\mathbb{V}\)
𝕍. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

Bookではhidden prop（Bookを美しくするために、表示したくはないけどprfでは何度も使われる補題）を使うこともできます。
ソース58行目のように !prop/thm と書いて紹介します。査読をクリックして、どんなpropが隠れているか確認してみて下さい。

1.5 クラスが集合となるか

次の(クラスを引数にした)述語を導入するのが自然です。
word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)

集合でないクラスは固有クラスと呼ばれます。最初の例はRussellクラスです（Matheliaでは「Russellのパラドクス」も定理になります）。
word(,c) … \(\mathbb{V}_0\)
𝕍0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O

ZFの多くの公理は、ある条件を満たすものの集まりが集合であることを主張します。Matheliaでは例えば「空集合公理」を次のように定理にする事が多いです。
ax_∅ … \(\dot\exists \{ x \mid {\perp} \}\) \(\blacktriangleleft\) ∅.

分出公理は「集合に含まれるクラスは集合である」ことを主張します。Matheliaでは次の1つのFormで表現できます。
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
宇宙も固有クラスであることが分かります。
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) ax_s
空集合公理 はax_sからも導出されます。
ax_∅ \(\blacktriangleleft\) ax_s