包含関係
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\)】
\({\subsetneq}.\)【\(X \subsetneq Y \Longleftrightarrow X \subsetneq Y\)】
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\(\blacktriangleleft\)
\({\subset}推\)【\(X \subset Y \subset Z \Longrightarrow X \subset Z\)】\(\blacktriangleleft\)
\({\subsetneq}推\)【\(X \subsetneq Y \subsetneq Z \Longrightarrow X \subsetneq Z\)】\(\blacktriangleleft\)
集合の全体、空集合
word(,c) … \(\text{Set}\)def …【\(\text{Set}\)】≃【\(\{ x \mid \top \} \)】
\(\text{Set0}\)【\(x \in \text{Set}\)】\(\blacktriangleleft\)
\(\text{Set1}\)【\(X \subset \text{Set}\)】\(\blacktriangleleft\)
word(,s) … \(\emptyset\)
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \} \)】
\(\emptyset0\)【\(x \notin \emptyset\)】\(\blacktriangleleft\)
\(\emptyset1\)【\(\emptyset \subset X\)】\(\blacktriangleleft\)
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】\(\blacktriangleleft\)
合併、共通部分、差
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\)】\(\blacktriangleleft\)
\({\subset}\text{a}\)【\(X \subset Y \Longleftrightarrow X \cap Y = X\)】\(\blacktriangleleft\)
総合併、総共通部分
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}\)】\(\blacktriangleleft\)
\(\cup_1\)【\(X = \bigcup \{ X \}\)】\(\blacktriangleleft\)
\(\cap_1\)【\(X = \bigcap \{ X \}\)】\(\blacktriangleleft\)
これも / D. で行けるように拡張したい。補題 \(\{X\} \neq \emptyset \) が必要。
\(\cup_2\)【\(X \cup Y = \bigcup \{ X , Y \}\)】\(\blacktriangleleft\)
\(\cap_2\)【\(X \cap Y = \bigcap \{ X , Y \}\)】\(\blacktriangleleft\)
集合は１点集合により分割されます。
\(\bigcup_1\)【\(X = \bigcup _{ x \in X } \{ x \}\)】\(\blacktriangleleft\)
べき集合
word(s,s) … \(\wp\)\(\wp.\)【\(\wp X = \{ A \mid A \subset X \} \)】
\(\wp\emptyset\)【\(\wp \emptyset = \{ \emptyset \}\)】\(\blacktriangleleft\)
分出公理
集合とクラスの共通部分は集合になります。が、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}\)】\(\blacktriangleleft\)
正則性公理
正則性公理。必要？\(\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 )\)】