1 - 1

論理

word(,p) … \(\top\)  \(\perp\)  
word(p,p) … \(\neg\)  
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Longrightarrow\)  \(\Leftrightarrow\)  \(\Longleftrightarrow\)  
word(q,p)R … \(\forall\)  \(\exists\)  
precedの差により\((\;)\)が略せることがあります。例　【\(\forall x \neg P\)】≈【\(\forall x ( \neg P )\)】

word関数 … 斜線をつける #/ : (\({\tt x}\)\({\tt y}\),p)→(\({\tt x}\)\({\tt y}\),p) ; (q,p)→(q,p)
def …【\({\sf A} \cancel{{\sf p}} {\sf B}\)】≃【\(\neg ( {\sf A} {\sf p} {\sf B} )\)】
def …【\(\not\forall {\sf x} {\sf P}\)】≃【\(\neg ( \forall {\sf x} {\sf P} )\)】,【\(\not\exists {\sf x} {\sf P}\)】≃【\(\neg ( \exists {\sf x} {\sf P} )\)】

論理の略記

abbr …【\( {\sf X} \)】≈【\({\sf X} , {\sf X}\)】
例　【\(x \in y \in z\)】≈【\(x \in y , y \in z\)】

abbr …【\({\sf T}_1,\cdots,{\sf T}_n\,{\sf A}\)】≈【\({\sf T}_1\,{\sf A},\cdots,{\sf T}_n\,{\sf A}\)】
例　【\(x , y \in X\)】≈【\(x \in X , y \in X\)】

abbr …【\( \forall {\sf x} {\sf A} . {\sf P} \)】≈【\(\forall {\sf x} \, ( {\sf x} {\sf A} \Rightarrow ( {\sf P} ) )\)】
abbr …【\( \exists {\sf x} {\sf A} . {\sf P} \)】≈【\(\exists {\sf x} \, ( {\sf x} {\sf A} , ( {\sf P} ) )\)】

abbr …【\(\forall{\sf x}_1,\cdots,{\sf x}_n.{\sf P}\)】≈【\(\forall{\sf x}_1\,\cdots \forall{\sf x}_n\,({\sf P})\)】
abbr …【\(\exists{\sf x}_1,\cdots,{\sf x}_n.{\sf P}\)】≈【\(\exists{\sf x}_1\,\cdots \exists{\sf x}_n\,({\sf P})\)】
abbr …【\(\forall{\sf x}_1,\cdots,{\sf x}_n{\sf A}.{\sf P}\)】≈【\(\forall{\sf x}_1{\sf A}.\,\cdots \forall{\sf x}_n{\sf A}.\,{\sf P}\)】
abbr …【\(\exists{\sf x}_1,\cdots,{\sf x}_n{\sf A}.{\sf P}\)】≈【\(\exists{\sf x}_1{\sf A}.\,\cdots \exists{\sf x}_n{\sf A}.\,{\sf P}\)】

下2つは未実装。\(\forall x,y\in\mathbb{M}.x+y\in\mathbb{M}\) 等も書けるよーに！

2項記号の操作

word関数 … 左右反転させる #- : (\({\tt x}\)\({\tt y}\),\({\tt z}\))→(\({\tt y}\)\({\tt x}\),\({\tt z}\))
def …【\({\sf A} \class{reflect}{{\sf p}} {\sf B}\)】≃【\({\sf B} {\sf p} {\sf A}\)】
表記は【\(X \class{reflect}{\notin} x\)】より【\(X \not\ni x\)】の方が良いでしょう。

word関数 … \(\widehat{\;\;}\) を付ける #2 : (\({\tt x}\)\({\tt x}\),\({\tt y}\))→(\({\tt x}\),\({\tt y}\))
def …【\(\widehat{{\sf p}} {\sf A}\)】≃【\({\sf p} {\sf A} {\sf A}\)】

クラスの生成(内包記法)、「要素である」

word(q,p)! …【\(\{ {\sf x} \mid {\sf P} \} \)】
abbr …【\(\{ {\sf x} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid {\sf x} {\sf A} , {\sf P} \} \)】
\(\sum_{i\in\{1,2\}}i=3\) の左辺を \(\sum\{i \mid i\in\{1,2\}\}\) と解釈するために次も準備します。
abbr …【\(_{ {\sf P} } {\sf x}\)】≈【\(\{ {\sf x} \mid {\sf P} \} \)】

word(ss,p) … \(\in\)  
word(sc,p) … \(\in\)  
def … 【\({\sf T} \in \{ {\sf x} \mid {\sf P} \} \)】≃\(【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}\)

word(s,c)! …【\( {\sf X} \)】
def …【\( {\sf X} \)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \} \)】

Form内で、Clsがあるべき所にSet \({\tt X}\) がある場合 {sc \({\tt X}\)} に変換されます。

等号

word(cc,p) … \(=\)  
def …【\({\sf C} = {\sf D}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf C} \Leftrightarrow {\sf x} \in {\sf D} )\)】
word(ss,p) … \(=\)  
\(=.\)【\(X = Y \Longleftrightarrow X = Y\)】

word(c,p) … \(\dot\exists\)  
def …【\(\dot\exists {\sf C}\)】≃【\(\exists {\sf x} \, ( {\sf x} = {\sf C} )\)】

Russelのパラドクスが「集合でないクラス(固有クラス)」の最初の例を与えます。
word(,c) … \(\text{Nsc}\)  
def …【\(\text{Nsc}\)】≃【\(\{ {\sf x} \mid {\sf x} \notin {\sf x} \} \)】
\(\text{nsc0}\)【\(\neg \dot\exists \text{Nsc}\)】◀ O