2 基本記号①

2.1 2項記号の操作

word+(\({\tt x}\)\({\tt y}\),\({\tt z}\)→\({\tt y}\)\({\tt x}\),\({\tt z}\)) … \(\leftrightarrow\)
lower … \(A \stackrel{\leftrightarrow}{\mathbin{{\sf p}}} B\) ≃ \(B \mathbin{{\sf p}} A\)
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→\({\tt x}\),\({\tt y}\)) … \(\prime\prime\)
lower … \(\stackrel{\prime\prime}{\mathbin{{\sf p}}} A\) ≃ \(A \mathbin{{\sf p}} A\)

word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[s,\({\tt x}\)][s,\({\tt x}\)],\({\tt y}\)) … \(\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x ( ( \mathbin{{\sf f}} x ) \mathbin{{\sf a}} ( \mathbin{{\sf g}} x ) )\)
word+(\({\tt x}\)\({\tt x}\),\({\tt y}\)→[ss,\({\tt x}\)][ss,\({\tt x}\)],\({\tt y}\)) … \(\star\!\star\)
lower … \([\mathbin{{\sf f}}] \stackrel{\star\!\star}{\mathbin{{\sf a}}} [\mathbin{{\sf g}}]\) ≃ \(\forall x , y ( ( x \mathbin{{\sf f}} y ) \mathbin{{\sf a}} ( x \mathbin{{\sf g}} y ) )\)

word+([ss,p][ss,p],[ss,p]) … \({\circ}\)
lower … \(x \, [\mathbin{{\sf p}}] {\circ} [\mathbin{{\sf q}}] \, z\) ≃ \(\exists y \, x \mathbin{{\sf p}} y \mathbin{{\sf q}} z\)

2.2 2項述語の性質

word+([ss,p],p)R … \(:\mathsf{R}\)  \(:\mathsf{T}\)  \(:\mathsf{X}\)
lower … \([\mathbin{{\sf p}}] :\mathsf{R}\) ≃ \(\forall x ( x \mathbin{{\sf p}} x )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{T}\) ≃ \(\forall x , y , z ( x \mathbin{{\sf p}} y \mathbin{{\sf p}} z \Longrightarrow x \mathbin{{\sf p}} z )\)
lower … \([\mathbin{{\sf p}}] :\mathsf{X}\) ≃ \(\forall x , y ( x \mathbin{{\sf p}} y \Longrightarrow y \mathbin{{\sf p}} x )\)
\([ \mathbin{p} ] :\mathsf{R} \Longleftrightarrow [=] \stackrel{\star\!\star}{\Rightarrow} [ \mathbin{p} ]\) \(\blacktriangleleft\) O
\([ \mathbin{p} ] :\mathsf{X} \Longleftrightarrow [\stackrel{\leftrightarrow}{\mathbin{p}}] \stackrel{\star\!\star}{\Rightarrow} [ \mathbin{p} ]\) \(\blacktriangleleft\) O
\([ \mathbin{p} ] :\mathsf{T} \Longleftrightarrow [ \mathbin{p} ] {\circ} [ \mathbin{p} ] \stackrel{\star\!\star}{\Rightarrow} [ \mathbin{p} ]\) \(\blacktriangleleft\) O
\([=] :\mathsf{R}\mathsf{T}\mathsf{X}\) \(\blacktriangleleft\) O

2.3 所属関係と内包記法

word(sc,p) … \(\in\)
word(ss,p) … \(\in\)

word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)
cvt … \(t \in \{ x \mid P \}\) ≃ substitution(\(P\), \(x\) ↦ \(t\))
abbr … \(\{ x \mathop{{\sf A}} \mid P \}\) ≈ \(\{ x \mid x \mathop{{\sf A}} , ( P ) \}\)

Form内でc-Formがあるべき所にあるs-Form \({\tt X}\) は \(\{x \mid x \in {\tt X}\}\) に置き換えられます(sc変換)。
\([\in] \stackrel{\star\!\star}{\Leftrightarrow} [\in]\) \(\blacktriangleleft\) O

2.4 外延性

=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
=. … \([=] \stackrel{\star\!\star}{\Leftrightarrow} [=]\)

\(X = \{ x \mid x \in X \}\) \(\blacktriangleleft\) O
\([ \mathbin{p} ] :\mathsf{R}\mathsf{T}\mathsf{X} \Longleftrightarrow \forall a , b \, a \mathbin{p} b \Longleftrightarrow \{ x \mid x \mathbin{p} a \} = \{ x \mid x \mathbin{p} b \}\) \(\blacktriangleleft\) O

2.5 包含関係

word(cc,p) … \(\subset\)  \(\subsetneq\)
⊂_. … \(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)
⊊_. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)

word(ss,p) … \(\subset\)  \(\subsetneq\)
⊂. … \([\subset] \stackrel{\star\!\star}{\Leftrightarrow} [\subset]\)
⊊. … \([\subsetneq] \stackrel{\star\!\star}{\Leftrightarrow} [\subsetneq]\)
⊊.. … \(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\) \(\blacktriangleleft\) \(\mathbb{W}.\)
\([\subset] :\mathsf{R}\mathsf{T}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
=.. … \(X = Y \Longleftrightarrow X \subset Y \subset X\) \(\blacktriangleleft\) \(\mathbb{W}.\)