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

1 論理記号

1.1 通常の論理word

word(,p) … \(\top\)  \({\perp}\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
word(vp,p)R … \(\forall\)  \(\exists\)
word(v_p,p)R … \(\forall\)  \(\exists\)
word(ss,p) … \(=\)
word(cc,p) … \(=\)

1.2 高度な論理word

word+(pp,p) … \({\bf ,}\,\)  \(\Longrightarrow\)  \(\Longleftrightarrow\)
lower … \(P {\bf ,}\, Q\) ≃ \(P , Q\)
lower … \(P \Longrightarrow Q\) ≃ \(P \Rightarrow Q\)
lower … \(P \Longleftrightarrow Q\) ≃ \(P \Leftrightarrow Q\)

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

1.3 andを含む省略記法

abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)
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} )\)

1.4 量化子の省略記法

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

2以上の自然数\({\tt n}\)に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)