等号
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
クラスの生成(超内包記法)
abbr …【\(\{ {\sf T} \mid {\sf P} \}\)】≈【\(\{ {\sf x} \mid \exists {\sf X} \, ( {\sf P} ) , {\sf x} = {\sf T} \} \)】例【\(\{ x \cup y \mid x , y \in X \}\)】≈【\(\{ z_{1} \mid \exists x , y \, ( x , y \in X ) , z_{1} = x \cup y \} \)】
\(\sum_{i\in\{0,1\}}(i+1)=3\) という記述もできるようにします。
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)を含まない。
{clsx ～ } 内で最初の | より前にword(ss,p)があるかどうかで、どちらの形か判断されます。
集合の生成(外延記法)
word(s\(^n\),s)! …【\(\{{\sf X}_1,\cdots,{\sf X}_n\}\)】\(\text{set}_n.\)【\(\{X_1,\cdots,X_n\}=\{x \mid x=X_1\mathbin{\rm o\!r}…\mathbin{\rm o\!r}x=X_n\}\)】
例えば【\(\{ x , \{ x , y \} \}\)】はSetで、現れる2つのsetはword(ss,s)です。
唯一の量化子
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} ) )\)】
包含関係
word(cc,p) … \(\subset\) \(\subsetneq\)def …【\({\sf C} \subset {\sf D}\)】≃【\( \forall {\sf x} \in {\sf C} . {\sf x} \in {\sf D} \)】
def …【\({\sf C} \subsetneq {\sf D}\)】≃【\({\sf C} \subset {\sf D} , {\sf C} \neq {\sf D}\)】
word(ss,p) … \(\subset\) \(\subsetneq\)
\(\subset.\)【\(X \subset Y \Longleftrightarrow X \subset Y\)】
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】/\(\subset.\)/\(=.\)◀ O
def …【\({\sf X} \subsetneq {\sf Y}\)】≃【\({\sf X} \subsetneq {\sf Y}\)】
\({\subset}\text{T}\)【\(X \subset Y \subset Z \Longrightarrow X \subset Z\)】/\(\subset.\)◀ O
\({\subsetneq}\text{T}\)【\(X \subsetneq Y \subsetneq Z \Longrightarrow X \subsetneq Z\)】/\(\subset.\)/\(=.\)◀ O