1
(集合論の言語だけでない)一般の一階言語に共通する記号を準備をします。
通常使用される記号以外にも多様な記号を用意し表現力を高めていきます。
命題記号、等号
word(,p) … \(\top\) \({\perp}\)word(p,p) … \(\neg\)
word(pp,p) … \(,\) \({\bf ,}\) \(\mathbin{\rm o\!r}\) \(\Rightarrow\) \(\Longrightarrow\) \(\Leftrightarrow\) \(\Longleftrightarrow\)
word(ss,p) … \(=\)
2以上の自然数 \({\tt n}\) に対し
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}}\)】
例 【\( x , y \in X\)】≈【\(x \in X , y \in X\)】
abbr* …【\( X\)】≈【\(X , X\)】
abbr* …【\( X\)】≈【\(X {\bf ,} \, X\)】
二項記号の処理
word関数 … 斜線をつける #/ : (\({\tt x}\)\({\tt y}\),p)→(\({\tt x}\)\({\tt y}\),p)cvt … 【\(A\!\not{\!{\sf p}}\,B\)】≃【\(\neg ( A \mathop{{\sf p}} B )\)】
word関数 … 左右反転させる #- : (\({\tt x}\)\({\tt y}\),\({\tt z}\))→(\({\tt y}\)\({\tt x}\),\({\tt z}\))
cvt …【\(A \class{reflect}{\mathop{{\sf p}}} B\)】≃【\(B \mathop{{\sf p}} A\)】
表記は【\(X \class{reflect}{\notin} x\)】より【\(X \not\ni x\)】の方が良いでしょう。
word関数 … \(\widehat{\;\;}\) を付ける #2 : (\({\tt x}\)\({\tt x}\),\({\tt y}\))→(\({\tt x}\),\({\tt y}\))
cvt …【\(\widehat{\mathop{{\sf p}}} \, A\)】≃【\(A \mathop{{\sf p}} A\)】
\({\sf p}"\)という表記に？
二項記号の関数化
abbr …【\(\mathop{{\sf f}} \,^\star{\mathop{{\sf a}}}\; \mathop{{\sf g}}\)】≈【\(\forall x \, ( \mathop{{\sf f}} x \mathop{{\sf a}} \mathop{{\sf g}} x )\)】
abbr …【\(\mathop{{\sf f}} \,^{\star\!\star}{\mathop{{\sf a}}}\; \mathop{{\sf g}}\)】≈【\(\forall x , y \, ( x \mathop{{\sf f}} y \mathop{{\sf a}} x \mathop{{\sf g}} y )\)】
量化記号
word(vp,p)R … \(\forall\) \(\exists\)1以上の自然数 \({\tt n}\) に対し
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 x_{\tt n} \, ( x_{1} \neq x_{2} , \cdots \Longrightarrow ( P ) )\)】
abbr …【\(\exists^* x_{1} , \cdots , x_{\tt n} P\)】≈【\(\exists x_{1} \cdots x_{\tt n} \, ( x_{1} \neq x_{2} , \cdots , ( 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 \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 , ( P ) )\)】
二項述語の一項述語
abbr …【\(\mathop{{\sf p}} {:}\, \text{I}\)】≈【\(\forall x \, ( x \mathop{{\sf p}} x )\)】abbr …【\(\mathop{{\sf p}} {:}\, \text{T}\)】≈【\(\forall x , y , z \, ( x \mathop{{\sf p}} y \mathop{{\sf p}} z \Longrightarrow x \mathop{{\sf p}} z )\)】
abbr …【\(\mathop{{\sf p}} {:}\, \text{X}\)】≈【\(\forall x , y \, ( x \mathop{{\sf p}} y \Longrightarrow y \mathop{{\sf p}} x )\)】
次のようなabbrは自動で準備されます。
abbr …【\(\mathop{{\sf p}} {:}\, \text{I} \text{T}\)】≈【\(\mathop{{\sf p}} {:}\, \text{I} , \mathop{{\sf p}} {:}\, \text{T}\)】
一階言語では論理が展開されます。最初の定理は「\(=\) は同値関係である」です。
【\(= {:}\, \text{I} \text{T} \text{X}\)】\(\blacktriangleleft\)
a2
代入
クラス
word(vp,c) … cls abbr …【\(\{ x \mid P \}\)】≈ cls $x ($P)abbr …【\(\{ x \mathop{{\sf A}} \mid P \}\)】≈【\(\{ x \mid x \mathop{{\sf A}} , P \}\)】
\(\sum_{i\in\{1,2\}}i=3\) の左辺を \(\sum\{i \mid i\in\{1,2\}\}\) と解釈するために次の準備をします。
abbr …【\(_{ P } x\)】≈【\(\{ x \mid P \}\)】
クラスの拡張をします。{cls …} 内で | | で挟まれた部分は表記では無視されます。
abbr …【\(\{ T \mid P \}\)】≈【\(\{ x \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}\)】
abbr …【\(\{ T \mathop{{\sf A}} \mid P \}\)】≈【\(\{ x \mathop{{\sf A}} \mid \exists \mathop{{\sf X}} \, ( ( P ) , x = T ) \}\)】
\(\sum_{i\in\{0,1\}}(i+1)=3\) という記述もできるようにします。
abbr …【\(_{ P } T\)】≈【\(\{ T \mid P \}\)】
word(sc,p) … \(\in\)
cvt…【\(T \in \{ x \mid P \}\)】≃【\(P^{x\,\mapsto\,T}\)】
一意性
word(vx,p)R … \(!\) \(\exists!\)am1.【\(! x P \Longleftrightarrow \forall y , z \in \{ x \mid P \} . y = z\)】
exi!.【\(\exists! x P \Longleftrightarrow \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 ) )\)】
アロー関数
word(vss,s) … fn abbr* …【\([ x \mapsto X ]\)】≈ fn $x ($X)【\([ x \mapsto X ] \, T\)】≃【\(X^{x\,\mapsto\,T}\)】
【\([ x \mapsto X ]\)】は一項関数と思えます。
第一引数を略して \(\bullet\) にできます。\(\mapsto\) も略されます。例 【\([ \bullet + a ]\)】≈【\([ x \mapsto x + a ]\)】
\(\bullet\) は入れ子では使用すべきでありませんが、必ず内側から計算されます。
例 【\([ \bullet + [ \bullet + x ] y ]\)】≃【\([ \bullet + ( y + x ) ]\)】