論理
word(,p) … \(\top\) \({\perp}\)word(p,p) … \(\neg\)
word(pp,p) … \(,\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(vp,p)R … \(\forall\) \(\exists\)
precedの差により\((\;)\)が略せることがあります。例 【\(\forall x \neg P\)】≈【\(\forall x ( \neg P )\)】
abbr …【\( {\sf X} \)】≈【\(( {\sf X} ) , ( {\sf X} )\)】
abbr … 【\({\sf T}_{1} , … , {\sf T}_{\tt n} {\sf A}\)】≈【\({\sf T}_{1} {\sf A} , … , {\sf T}_{\tt n} {\sf A}\)】
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}_{\tt n} \, {\sf P}\)】≈【\(\forall {\sf x}_{1} \cdots \forall {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\(\exists {\sf x}_{1} , \cdots , {\sf x}_{\tt n} \, {\sf P}\)】≈【\(\exists {\sf x}_{1} \cdots \exists {\sf x}_{\tt n} ( {\sf P} )\)】
abbr … 【\(\forall {\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 … 【\(\exists {\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} \)】
例 【\(\forall x , y \in M . x \cup y \in M\)】≈【\(\forall x \, \forall y \, ( x \in M \Rightarrow ( y \in M \Rightarrow x \cup y \in M ) )\)】
word関数
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関数 … 左右反転させる #- : (\({\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)! …【\(\{ {\sf x} \mid {\sf P} \} \)】
abbr …【\(_{ {\sf P} } {\sf x}\)】≈【\(\{ {\sf x} \mid {\sf P} \} \)】
abbr …【\(\{ {\sf x} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid {\sf x} {\sf A} , {\sf P} \} \)】
word(sc,p) … \(\in\)
def … 【\({\sf T} \in \{ {\sf x} \mid {\sf P} \} \)】≃\(【{\sf P}】\!^{{\sf x}\,\mapsto\,{\sf T}}\)
word(ss,p) … \(\in\)
集合はクラスとみなされます。
word(s,c)! …【\( {\sf X} \)】
def …【\( {\sf X} \)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \} \)】
scは省略可能です。例 【\(x \in X\)】≃【\(x \in X\)】
等号
word(cc,p) … \(=\)def …【\({\sf X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} \Leftrightarrow {\sf x} \in {\sf Y} )\)】
word(ss,p) … \(=\)
\({=.}\)【\(X = Y \Longleftrightarrow X = Y\)】
\(\Longleftarrow\) は外延性公理と呼ばれるものです。
内包記法が拡張されます。
abbr …【\(\{ {\sf T} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid \exists {\sf X} \, ( ( {\sf P} ) , {\sf x} = {\sf T} ) \} \)】
abbr …【\(_{ {\sf P} } {\sf T}\)】≈【\(\{ {\sf T} \mid {\sf P} \}\)】
abbr …【\(\{ {\sf T} {\sf A} \mid {\sf P} \}\)】≈【\(\{ {\sf x} {\sf A} \mid \exists {\sf X} \, ( {\sf P} ) , {\sf x} = {\sf T} \}\)】
条件 : \({\sf T}\)の代入先はword(ss,p)を含まない。
唯一の量化子
word(vx,p)R … \(!\) \(\exists!\)def …【\(! {\sf x} {\sf P}\)】≃【\(\forall {\sf y} , {\sf z} \in \{ {\sf x} \mid {\sf P} \} . {\sf y} = {\sf z}\)】
def …【\(\exists! {\sf x} {\sf P}\)】≃【\(\exists {\sf x} \, {\sf P} , ! {\sf x} {\sf P}\)】
abbr …【\( ! {\sf x} {\sf A} . {\sf P} \)】≈【\(! {\sf x} \, ( {\sf x} {\sf A} , ( {\sf P} ) )\)】
abbr …【\( \exists! {\sf x} {\sf A} . {\sf P} \)】≈【\(\exists! {\sf x} \, ( {\sf x} {\sf A} , ( {\sf P} ) )\)】