1 集合・クラスの基本

1.1 所属関係

集合は現代の抽象数学の基礎概念と言え、その公理系については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.2 包含関係

ここでも「集合の包含関係」と「クラスの包含関係」の２つがあります。
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\)

default.thmelでもslashは有効です。\({\tt P}\) / \({\tt Q}\) は「\({\tt P}\)|cvt を \({\tt Q}\)|cvt で展開したもの」です。ソース35行目で / W. が使われています。
\(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)

1.3 宇宙、空集合

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では何度も使われる補題）を使うこともできます。
ソース54行目のように !prop/thm と書いて紹介します。査読をクリックして、どんなpropが隠れているか確認してみて下さい。

1.4 クラスが集合となるか

次の(クラスを引数にした)述語を導入するのが自然です。
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