この本及びimportしているword_logic.bookはarticlesの各本で共通して使われる記号の表です。
tex表記されたものをクリックするとソースが出てきます。こまめに（特に疑問を感じた時は）確認して下さい。
\(P\) ◀ \(\Gamma\) が「前提 \(\Gamma\) から \(P\) が示される」と意味すること、などはtutorialに書かれています。
\(\mathbb{W}.\) は、その位置までに置かれた定義の列ですが、この本の終わりでは \(\subset.\) と \(=.\) の2つになります。

1 基本記号

1.1 内包記法

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 ) \}\)
abbr … \(_{ P } T\) ≈ \(\{ T \mid P \}\)

1.2 所属関係、等号、包含関係

word(sc,p) … \(\in\)
word(ss,p) … \(\in\)
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))
集合はクラスと同一視されます。Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。

=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
=. … \(X = Y \Longleftrightarrow X = Y\)

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\)

1.3 クラスが集合になるか

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.4 一意量化子

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 ) )\)

1.5 関数の像

word+(s,s→s,c) … \(\text{^}\)
lower … \(\stackrel{\text{^}}{\mathbin{{\sf f}}} A\) ≃ \(\{ \mathbin{{\sf f}} a \mid a \in A \}\)
word+(ss,s→ss,c) … \(\text{^*}\)  \(\text{*^}\)  \(\text{^^}\)
lower … \(A \stackrel{\text{^*}}{\mathbin{{\sf f}}} b\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A \}\)
lower … \(a \stackrel{\text{*^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid b \in B \}\)
lower … \(A \stackrel{\text{^^}}{\mathbin{{\sf f}}} B\) ≃ \(\{ a \mathbin{{\sf f}} b \mid a \in A , b \in B \}\)

1.6 アロー関数

word(vs,(s,s))F … \(\mathsf{fn}\)
abbr … \(\lceil x \mapsto X \rfloor\) ≈ \(\mathsf{fn} ( x , X )\)
cvt … \(\lceil x \mapsto X \rfloor ( t )\) ≃ substitution(\(X\), \(x\) ↦ \(t\))
\(\mapsto\) の前のv-Formを \(\bullet\) に替えられます。その際 \(\bullet \mapsto\) は略されます。例　 \(\lceil \bullet + a \rfloor\) ≈ \(\lceil x \mapsto x + a \rfloor\)