このフォルダの本は、準備の本の上に定理を1つずつ示す記事です（100の数学定理 から選んだものが多い）。
この本はフォルダの各本で共通して使われる記号の表です。
\(P\) ◀ \(\Gamma\) が「前提 \(\Gamma\) から \(P\) が示される」と意味すること、などはtutorialに書かれています。
\(\mathbb{W}.\) は、この本の終わりでは \(\subset.\) と \(=.\) の2つになります。
読み方（人間向けの要点）：
　〇 主張は \(P\) ◀ \(\Gamma\) の形で、\(\Gamma\) に並ぶのは使ってよい公理・定義の名前です。\(\mathbb{W}.\) はその位置までに本（と import した本）が置いた定義の列で、本ごとに中身が違います。
　〇 \(\mathbb{M}\) は 0 から始まる自然数です（集合で作る本と、公理で与える本があります）。\(n\) の後続 \({\rm suc}(n)\) は斜体の \(n+1\) で表示されます。
　〇 式の中の \(,\) は「かつ」、\(\dot\exists C\) は「クラス \(C\) が集合である」です（下の各節）。

1 論理〜分出公理

1.1 論理記号

word(,p) … \(\top\)  \({\perp}\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
ここでの \(,\) は「かつ」（ソースは and）。
word+(pp,p) … \(\Longrightarrow\)  \(\Longleftrightarrow\)
lower … \(P \Longrightarrow Q\) ≃ \(P \Rightarrow Q\)
lower … \(P \Longleftrightarrow Q\) ≃ \(P \Leftrightarrow Q\)
word(vp,p)R … \(\forall\)  \(\exists\)

1.2 省略記法

word+(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)

abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
abbr … \(X_{1} \mathbin{{\sf p}_{1}} X_{2} \cdots \mathbin{{\sf p}_{\tt n\,{\text -}\,1}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}_{1}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}_{\tt n\,{\text -}\,1}} X_{\tt n} )\)

abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
abbr … \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} , ( P ) )\)

1.3 2項述語

word(sc,p) … \(\in\)
word(cc,p) … \(\subset\)  \(=\)
⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)

word(ss,p) … \(\in\)  \(\subset\)  \(=\)
表記上は区別をされないので注意（クラスに関わる方はソースに _ が付く）。

1.4 内包記法

word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)
abbr … \(\{ T \mid P \}\) ≈ \(\{ x \mid \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)
abbr … \(\{ T \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , \exists \mathop{{\sf X}} ( ( P ) , x = T ) \}\)

cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))

1.5 集合をクラスと見なすこと

Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
集合の包含・等号はクラスの包含・等号から誘導します。
⊂. … \(X \subset Y \Longleftrightarrow X \subset Y\)
=. … \(X = Y \Longleftrightarrow X = Y\)

word(c,p) … \(\dot\exists\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
ax_s … \(\exists X \, C \subset X \Longrightarrow \dot\exists C\)
\(\dot\exists C\) は「クラス \(C\) が集合である」。ax_s（分出公理）は「集合に含まれるクラスは集合である」。
値が集合になる語（集合の語）の定義は、そのクラスが集合であること（存在）も含みます。

1.6 一意量化子

\(! x P\) は「\(P\) を満たす \(x\) は高々1つ」、\(\exists! x P\) は「ちょうど1つ」。
abbr … \(! x P\) ≈ \(\forall y , z \in \{ x \mid P \} . y = z\)
abbr … \(\exists! x P\) ≈ \(\exists x P , ! x P\)
abbr … \(! x \mathop{{\sf A}} . P\) ≈ \(! x ( x \mathop{{\sf A}} , ( P ) )\)
abbr … \(\exists! x \mathop{{\sf A}} . P\) ≈ \(\exists! x ( x \mathop{{\sf A}} , ( P ) )\)