1 この Book の読み方

この Book は、Mathelia で集合論の最初の部分（所属・包含・宇宙・空集合・べき集合・和と積・ZF の公理）を書いた例です。ヘッダは import /common/word_basis（集合論の基本の語を読み込む）です（thmel 行は書かないので default.thmel を読みます）。
表示では ∈ と ∈_、= と =_、⊂ と ⊂_、X と X_ が同じ形になり、prf は表示されません。そこで各 Thm の直後に「ソース：」の行で thm と prf のソースを載せています（字下げした prf の続きの行は「　　」で示す）。
この Book の prf は、ほぼ次の型のどれかです。

prf の型（ソース）	何をしているか	主な例
goal -| O p;	-| の変換（|cvt+、5.book）が、クラスの語（𝕍・=_ など）の定義と内包を開いてから Prover9 へ	2.1・3.1・5.1
goal / W. -| O p; goal -| W. h;（/ は1〜4本）	W.（集合の語の定義）で展開してから投げ、h; で「◀ W.」の形に戻す（4.book）。/ の本数は開く回数	2.2・3.1・3.3・4.1
goal -| ⋃. p; goal -| W. h;	必要な定義だけを sos に置いて投げ、h; で W. の形に	5.1
goal --| ax_s v;	クラス変数を含む公理を前提に、{s,c}ソートのまま Vampire へ（5.book）	6.1
goal --| ax_r[??p^:=`…`] v; と … ◀ ax_r h;	公理図式（schema）の実例を段の sos に直接書いて前提に使い、h; で「ax_r から導かれる」形に	6.3
ax_∅ -| ∅. p;	最後の段が thm と同じ goal・sos なので h; は無い（3.book）	5.2
/// W.'	〇.' があればそれで展開する slash（4.3）	4.3

!prop/thm・!prop の ! は「表示しない」印です（証明で使う補題など）。h; の段の関係の選び方は 3.book「h; の段の関係」。

2 基本関係

2.1 所属関係

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

Formel では「集合」と「クラス」を同一視して（いるように）扱えます（option ではなく組み込みの sc 変換）。
Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。

次の自明に見える定理が生まれます。
\(X \in Y \Longleftrightarrow X \in Y\) \(\blacktriangleleft\) O
　ソース：thm `X ∈ Y ⟺ X ∈_ Y` ◀ O　prf goal -| O p;
高度な表現を使うと \([\in] \stackrel{\star\!\star}{\Leftrightarrow} [\in]\)
\(X = \{ x \mid x \in X \}\) \(\blacktriangleleft\) O
　ソース：thm `X =_ \{ cls x | x ∈ X \}` ◀ O　prf goal -| O p;

（通常の数学の教科書とは逆に）\(=\) の定義は \(=\) の定義から誘導するのが自然です（表示ではどちらも = です。ソースでは =＝集合の等号、=_＝クラスの等号）。定義 =. は \(X = Y \Longleftrightarrow X = Y\) （word_basis で紹介済み）。

2.2 包含関係

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

\(\subset\)の定義 ⊂. も\(\subset\)の定義から誘導されます（ \(X \subset Y \Longleftrightarrow X \subset Y\) ・word_basis で紹介済み）（ソースでは ⊂ と ⊂_。表示ではどちらも ⊂ です）。
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm =.. ◀ W.　prf =.. / W. -| O p; =.. -| W. h;
\({\tt P}\) / \({\tt Q}\) は「\({\tt P}\)|cvt を \({\tt Q}\)|cvt で展開したもの」とされます。

3 集合・クラスの例①

3.1 宇宙、空集合

word(,c) … \(\mathbb{V}\)
𝕍. … \(\mathbb{V} = \{ x \mid \top \}\)
∈_𝕍 … \(x \in \mathbb{V}\) \(\blacktriangleleft\) O
　ソース：prop/thm ∈_𝕍 <- `x ∈_ 𝕍` ◀ O　prf ∈_𝕍 -| O p;
⊂_𝕍 … \(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
　ソース：prop/thm ⊂_𝕍 <- `X ⊂_ 𝕍` ◀ O　prf ⊂_𝕍 -| O p;

word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
∉∅ … \(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm ∉∅ <- `x {/}∈ ∅` ◀ W.　prf ∉∅ / W. -| O p; ∉∅ -| W. h;
∅⊂ … \(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm ∅⊂ <- `∅ ⊂ X` ◀ W.　prf ∅⊂ // W. -| O p; ∅⊂ -| W. h;
prfの / の本数は \(\mathbb{W}.\) を適用する回数です。足りないと証明が見つからず FAIL になります。例えば \(X \cap Y \subset X\) ◀ W. は goal / W. -| O p; では FAIL、goal // W. -| O p; では OK です（∩ は 4.2 で紹介します）。迷ったら slash_cli で開き残りの語が無いかを見てから本数を決めます（4.book）。

3.2 外延記法

Formel ではword familyも使用できます。指定した元だけを持つ集合を作ります。1以上の自然数 \({\tt n}\) に対して
word(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
Formelは \(\cdots\) や \({\tt n}\) はしかるべく処理します。例　 \(\{ x , \{ x , y \} \}\) ≈ \(\mathsf{set}_{2} ( x , \mathsf{set}_{2} ( x , y ) )\)

定義familyも使用できます。Bookで次のset\({\tt n}\).が紹介されると \(\mathbb{W}.\) は無限列になります。
set\({\tt n}\). … \(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)

3.3 べき集合

word(s,s) … \(\wp\)
℘. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm wp0 ◀ W.　prf wp0 //// W. -| O p; wp0 -| W. h;