共通の記号
admin
この本はarticlesの各本で共通して使われる記号の表です。section 1 だけ（論理記号）を使うなら
import /common/word0:1、section 2 まで（基本記号）なら
import /common/word0:2 と書きます。
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(v^p,p)R …
\(\forall\)word(?v^p,p)R …
\(\forall\)word(??v^p,p)R …
\(\forall\)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 ) )\) 2 基本記号
2.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 \}\) 2.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\) 2.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（分出公理）は「集合に含まれるクラスは集合である」。
2.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 ) )\) 2.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 \}\) 2.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\) 3 集合
3.1 基本的な集合関数
word(,s) …
\(\emptyset\)∅. …
\(\emptyset = \{ x \mid {\perp} \}\) word(s\(^{\tt n}\),s)F …
\(\mathsf{set}_{\tt n}\)abbr …
\(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈
\(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\) 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} \}\) word(ss,s) …
\(\cup\) \(\cap\)∪. …
\(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\) ∩. …
\(X \cap Y = \{ x \in X \mid x \in Y \}\) 3.2 順序対、直積、写像
word(ss,s)F …
\(\mathsf{pr}\)abbr …
\(\langle X , Y \rangle\) ≈
\(\mathsf{pr} ( X , Y )\) word(s,s) …
\(\triangleleft\) \(\triangleright\)◁. …
\(\triangleleft \langle x , y \rangle = x\) ▷. …
\(\triangleright \langle x , y \rangle = y\) pr:0 …
\(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)word(ss,s) …
\(\times\) \(\to\)^^pr. …
\(X \times Y = \{ \langle x , y \rangle \mid x \in X , y \in Y \}\) →. …
\(X \to Y = \{ f \subset X \times Y \mid \forall x \in X . \exists! y \, \langle x , y \rangle \in f \}\) word(ss,s) …
*^ap*^ap. …
\(R ( A ) = \{ y \mid \exists x \in A . \langle x , y \rangle \in R \}\)