集合の全体、空集合
word(,c) … \(\text{Set}\)def …【\(\text{Set}\)】≃【\(\{ {\sf x} \mid \top \} \)】
\(\text{Set0}\)【\(x \in \text{Set}\)】◀ O
\(\text{Set1}\)【\(X \subset \text{Set}\)】◀ O
word(,s) … \(\emptyset\)
\(\emptyset.\)【\(\emptyset = \{ x \mid {\perp} \} \)】
\(\emptyset0\)【\(x \notin \emptyset\)】/\(\emptyset.\)◀ O
\(\emptyset1\)【\(\emptyset \subset X\)】/\(\subset.\)/\(\emptyset.\)◀ O
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】◀ \(=.\)\(\emptyset0\)
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\) \(\mathop\setminus\)def …【\({\sf C} \cup {\sf D}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf C} \mathbin{\rm o\!r} {\sf x} \in {\sf D} \} \)】
def …【\({\sf C} \cap {\sf D}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf C} , {\sf x} \in {\sf D} \} \)】
def …【\({\sf C} \mathop\setminus {\sf D}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf C} , {\sf x} \notin {\sf D} \} \)】
word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
\(\cup.\)【\(X \cup Y = X \cup Y\)】
\(\cap.\)【\(X \cap Y = X \cap Y\)】
\(\setminus.\)【\(X \mathop\setminus Y = X \mathop\setminus Y\)】
\({\subset}\text{u}\)【\(X \subset Y \Longleftrightarrow X \cup Y = Y\)】/\(\subset.\)/\(=.\)/\(\cup.\)◀ O
\({\subset}\text{a}\)【\(X \subset Y \Longleftrightarrow X \cap Y = X\)】/\(\subset.\)/\(=.\)/\(\cap.\)◀ O
総合併、総共通部分
word(c,c) … \(\bigcup\) \(\bigcap\)def …【\(\bigcup {\sf C}\)】≃【\(\{ {\sf x} \mid \exists {\sf y} \in {\sf C} . {\sf x} \in {\sf y} \} \)】
def …【\(\bigcap {\sf C}\)】≃【\(\{ {\sf x} \mid \forall {\sf y} \in {\sf C} . {\sf x} \in {\sf y} \} \)】
word(s,s) … \(\bigcup\) \(\bigcap\)
\(\bigcup.\)【\(\bigcup X = \bigcup X\)】
\(\bigcap.\)【\(X \neq \emptyset \Longrightarrow \bigcap X = \bigcap X\)】
\(\bigcap\emptyset\)【\(\bigcap \emptyset = \text{Set}\)】/\(\emptyset.\)◀ O
\(\cup_1\)【\(X = \bigcup \{ X \}\)】/\(=.\)/\(\bigcup.\)/\(\text{set}_1.\)◀ O
\(\cap_1\)【\(X = \bigcap \{ X \}\)】/\(=.\)/\(\bigcap.\)/\(\text{set}_1.\)◀ O
\(\cup_2\)【\(X \cup Y = \bigcup \{ X , Y \}\)】/\(=.\)/\(\cup.\)/\(\bigcup.\)/\(\text{set}_2.\)◀ O
\(\cap_2\)【\(X \cap Y = \bigcap \{ X , Y \}\)】/\(=.\)/\(\cap.\)/\(\bigcap.\)/\(\text{set}_2.\)◀ O
集合は１点集合により分割されます。
\(\text{sep_set}\)【\(X = \bigcup _{ x \in X } \{ x \}\)】/\(=.\)◀ \(\text{set}_1.\)
べき集合
word(s,s) … \(\wp\)\(\wp.\)【\(\wp X = \{ A \mid A \subset X \} \)】
\(\wp0\)【\(\wp \emptyset = \{ \emptyset \}\)】/\(=.\)/\(\wp.\)/\(\text{set}_1.\)/\({=}{.}{.}\)◀ \(\emptyset1\)
分出公理
集合とクラスの共通部分は集合になります。が、word(sc,s)は使用できません。無限個の公理が必要なのは頭の痛い所です。word(c,p)F … \(\text{axs}\)
def …【\(\text{axs} ( {\sf C} )\)】≃【\(\forall {\sf x} \, \dot\exists ( {\sf x} \cap {\sf C} )\)】
\(\text{nsc1}\)【\(\neg \dot\exists \text{Set}\)】◀ \(\text{axs} ( \text{Nsc} )\)
正則性公理
正則性公理。必要？\(\text{axr}\)【\( \forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset \)】
axr! = axr / emp.. / cap.
\(\text{wfs}_1\)【\(X \notin X\)】
\(\text{wfs}_2\)【\(\neg ( X \in Y \in X )\)】