等号
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\)】
\(\Longleftarrow\) は外延性公理と呼ばれるものです。
クラスに対して「集合である」という述語があります。
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}\)】\(\blacktriangleleft\)
クラスの生成(超内包記法)
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} \cdots \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} ) )\)】
2項述語の述語
擬順序関係abbr …【\({\sf p} \cdots \text{自}\)】≈【\(\forall {\sf x} \, ( {\sf x} \, {\sf p} \, {\sf x} )\)】
abbr …【\({\sf p} \cdots \text{推}\)】≈【\(\forall {\sf x} , {\sf y} , {\sf z} \, ( {\sf x} \, {\sf p} \, {\sf y} \, {\sf p} \, {\sf z} \Longrightarrow {\sf x} \, {\sf p} \, {\sf z} )\)】
abbr …【\({\sf p} \cdots \text{自推}\)】≈【\({\sf p} \cdots \text{自} , {\sf p} \cdots \text{推}\)】
同値関係
abbr …【\({\sf p} \cdots \text{対}\)】≈【\(\forall {\sf x} , {\sf y} \, ( {\sf x} \, {\sf p} \, {\sf y} \Rightarrow {\sf y} \, {\sf p} \, {\sf x} )\)】
abbr …【\({\sf p} \cdots \text{EQ}\)】≈【\({\sf p} \cdots \text{自推} , {\sf p} \cdots \text{対}\)】
\({=}\text{EQ}\)【\(= \cdots \text{EQ}\)】\(\blacktriangleleft\)
順序関係
abbr …【\({\sf p} \cdots \text{同}\)】≈【\(\forall {\sf x} , {\sf y} \, ( {\sf x} \, {\sf p} \, {\sf y} \, {\sf p} \, {\sf x} \Longrightarrow {\sf x} = {\sf y} )\)】
abbr …【\({\sf p} \cdots \text{ORD}\)】≈【\({\sf p} \cdots \text{自推} , {\sf p} \cdots \text{同}\)】
\({=}\text{ORD}\)【\(= \cdots \text{ORD}\)】\(\blacktriangleleft\)