論理
word(,p) … \(\top\) \({\perp}\)word(p,p) … \(\neg\)
word(pp,p) … \(,\) \(\mathbin{\rm o\!r}\) \(\) \(\) \(\) \(\)
word(vp,p)R … \(\forall\) \(\exists\)
precedの差により\((\;)\)が略せることがあります。例 【\(\forall x \neg P\)】≈【\(\forall x ( \neg P )\)】
word関数 … 斜線をつける #/ : (\({\tt x}\)\({\tt y}\),p)→(\({\tt x}\)\({\tt y}\),p)
def …【\({\sf A} \cancel{\mathop{{\sf p}}} {\sf B}\)】≃【\(\neg ( {\sf A} \mathop{{\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} )\)】 word(,p) … \(\top\) \({\perp}\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\) \(\mathbin{\rm o\!r}\) \(\) \(\) \(\) \(\)
word(vp,p)R … \(\forall\) \(\exists\)
precedの差により\((\;)\)が略せることがあります。例 【\(\forall x \neg P\)】≈【\(\forall x ( \neg P )\)】
word関数 … 斜線をつける #/ : (\({\tt x}\)\({\tt y}\),p)→(\({\tt x}\)\({\tt y}\),p)
def …【\({\sf A} \cancel{\mathop{{\sf p}}} {\sf B}\)】≃【\(\neg ( {\sf A} \mathop{{\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} , … , {\sf T}_{\tt n} \mid {\sf A}\)】≈【\({\sf T}_{1} {\sf A} , … , {\sf T}_{\tt n} {\sf A}\)】
例 【\( x , y \mid \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} ) )\)】
all, exi はその前が { ならtokenです。{ } 内に . を含みます。
abbr … 【\( {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\( {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\( {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\forall {\sf x}_{1} {\sf A} . \cdots \forall {\sf x}_{\tt n} {\sf A} . {\sf P}\)】
abbr … 【\( {\sf x}_{1} , \cdots , {\sf x}_{\tt n} {\sf A} . {\sf P}\)】≈【\(\exists {\sf x}_{1} {\sf A} . \cdots \exists {\sf x}_{\tt n} {\sf A} . {\sf P}\)】
{alls ～ } や {exis ～ } 内に . を含むかどうかで、どちらの形か判定されます。
例 【\( x , y \in M . x \cup y \in M\)】≈【\(\forall x \, \forall y \, ( x \in M ( y \in M x \cup y \in M ) )\)】
2項記号の操作
word関数 … 左右反転させる #- : (\({\tt x}\)\({\tt y}\),\({\tt z}\))→(\({\tt y}\)\({\tt x}\),\({\tt z}\))def …【\({\sf A} \class{reflect}{\mathop{{\sf p}}} {\sf B}\)】≃【\({\sf B} \mathop{{\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{\mathop{{\sf p}}} \, {\sf A}\)】≃【\({\sf A} \mathop{{\sf p}} {\sf A}\)】
クラスの生成(内包記法)
word(vp,c)! …【\(\{ Array {\sf x} \mid {\sf P} \}\)】\(\sum_{i\in\{1,2\}}i=3\) の左辺を \(\sum\{i \mid i\in\{1,2\}\}\) と解釈するために次も準備します。
abbr …【\(_{ {\sf P} } {\sf x}\)】≈【\(\{ Array {\sf x} \mid {\sf P} \}\)】
abbr …【\(\{ Array {\sf x} {\sf A} \mid {\sf P} \}\)】≈【\(\{ Array {\sf x} \mid {\sf x} {\sf A} , {\sf P} \}\)】
cls は2つ次の単語が | でなければtokenです。
集合、クラスの基本
word(ss,p) … \(\in\)word(sc,p) … \(\in\)
def … 【\({\sf T} \in \{ Array {\sf x} \mid {\sf P} \}\)】≃\(【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}\)
集合はクラスとみなされます。
word(s,c)! …【\( {\sf X}\)】
def …【\( {\sf X}\)】≃【\(\{ Array {\sf x} \mid {\sf x} \in {\sf X} \}\)】
scは省略可能です。例 【\(x \in X\)】≃【\(x \in X\)】