a1
数学の基盤となる集合・クラスの話から始めます。集合はZFに準拠します。\(\dagger\)
クラスはZFでは扱えませんが当システムでは自然に使えます。
基本的な関係
word(ss,p) … \(\in\)クラスの等号として次が使用されます。
word(cc,p) … \(=\)
=_.【\(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)】
「集合をクラスとみなす」ことが良く行われます。
word(s,c) … \(\text{sc}\)
sc.【\(\text{sc} ( X ) = \{ x \mid x \in X \}\)】
次のような計算が多用されます。 【\(x \in \text{sc} ( X )\)】≃【\(x \in X\)】
Form内で、(gramから推測して)c-Formがあるべき所にあるとき、scは省略可能とされます。
必要に応じ \({\tt X}\) は sc \({\tt X}\) に変換されます(sc補完)。\(\dagger\) 例 【\(x \in X\)】→【\(x \in \text{sc} ( X )\)】
集合の等号としては =s ≅ = が使用されます。次の式(の\(\Leftarrow\))は外延性公理です。
=s.【\(= \,^{\star\!\star}{\Leftrightarrow}\; =\)】
包含関係
word(cc,p) … \(\subset\) \(\subsetneq\)sub_.【\(X \subset Y \Longleftrightarrow \forall x \in X . x \in Y\)】
subn_.【\(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)】
word(ss,p) … \(\subset\) \(\subsetneq\)
sub.【\(\subset \,^{\star\!\star}{\Leftrightarrow}\; \subset\)】
subn.【\(\subsetneq \,^{\star\!\star}{\Leftrightarrow}\; \subsetneq\)】
subn..【\(X \subsetneq Y \Longleftrightarrow X \subset Y , X \neq Y\)】\(\blacktriangleleft\)
【\(\subset {:}\, \text{I} \text{T}\)】\(\blacktriangleleft\)
=s..【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\(\blacktriangleleft\)
【\(( X \subsetneq Y \subset Z ) \mathbin{\rm o\!r} ( X \subset Y \subsetneq Z ) \Longrightarrow X \subsetneq Z\)】\(\blacktriangleleft\)
宇宙、空集合
word(,c) … \(\mathbb{V}\)\V.【\(\mathbb{V} = \{ x \mid \top \}\)】
【\(x \in \mathbb{V}\)】\(\blacktriangleleft\)
【\(X \subset \mathbb{V}\)】\(\blacktriangleleft\)
word(,s) … \(\emptyset\)
\0.【\(\emptyset = \{ x \mid {\perp} \}\)】
【\(x \notin \emptyset\)】\(\blacktriangleleft\)
【\(\emptyset \subset X\)】\(\blacktriangleleft\)
\0..【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】\(\blacktriangleleft\)
有限集合
1以上の自然数 \({\tt n}\) に対してword(s\(^{\tt n}\),s)F … set\({\tt n}\) abbr …【\(\{ x_{1} , \cdots , x_{\tt n} \}\)】≈ set\({\tt n}\) ($x1 , … , $xn)
例 【\(\{ x , \{ x , y \} \}\)】≈ set2 (x , set2 (x , y))
set\({\tt n}\).【\(\{ x_{1} , \cdots , x_{\tt n} \} = \{ v \mid v = x_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} v = x_{\tt n} \}\)】
集合の有限集合を作るときには sets ≅ set を使用します。
sets\({\tt n}\).【\(\{ X_{1} , \cdots , X_{\tt n} \} = \{ V \mid V = X_{1} \mathbin{\rm o\!r} \cdots \mathbin{\rm o\!r} V = X_{\tt n} \}\)】
a2
集合・クラスの初等関数を作ります。
集合から集合を作るもの、クラスからクラスを作るもの、関数から関数を作るものがあります。
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\)cup_.【\(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)】
cap_.【\(X \cap Y = \{ x \mid x \in X , x \in Y \}\)】
word(c,c) … \(\mathop\setminus\)
xs.【\(\mathop\setminus Y = \{ x \mid x \notin Y \}\)】
word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
cup.【\(\cup \,^{\star\!\star}{=}\; \cup\)】
cap.【\(\cap \,^{\star\!\star}{=}\; \cap\)】
dif.【\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\)】
【\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\)】\(\blacktriangleleft\)
総合併、総共通部分
word(c,c) … \(\bigcup\) \(\bigcap\)Cup_.【\(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)】
Cap_.【\(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)】
【\(\bigcap \emptyset = \mathbb{V}\)】\(\blacktriangleleft\)
word(s,s)R … \(\bigcup\) \(\bigcap\)
Cup.【\(\bigcup \,^\star{=}\; \bigcup\)】
Cap.'【\(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)】
【\(X = \bigcup \{ X \}\)】\(\blacktriangleleft\)
【\(X = \bigcap \{ X \}\)】\(\blacktriangleleft\)
【\(X \cup Y = \bigcup \{ X , Y \}\)】\(\blacktriangleleft\)
【\(X \cap Y = \bigcap \{ X , Y \}\)】\(\blacktriangleleft\)
集合は１点集合により分割されます。
【\(X = \bigcup _{ x \in X } \{ x \}\)】\(\blacktriangleleft\)
べき集合
word(s,s) … \(\wp\)wp.【\(\wp X = \{ A \mid A \subset X \}\)】
wp0【\(\wp \emptyset = \{ \emptyset \}\)】\(\blacktriangleleft\)
wp1【\(\wp \{ x \} = \{ \emptyset , \{ x \} \}\)】\(\blacktriangleleft\)
関数の像
word関数 … 表記の無い #p : (s,s)→(s,c)cvt …【\({\mathop{{\sf f}}} \, A\)】≃【\(\{ \mathop{{\sf f}} a \mid a \in A \}\)】
【\(\dot\exists \, {\mathop{{\sf f}}} \, A\)】というのが置換公理です(？)
word関数 … 表記の無い #l , #r , #P : (ss,s)→(ss,c)
cvt …【\(A \, {\mathop{{\sf f}}} \, b\)】≃【\(\{ a \mathop{{\sf f}} b \mid a \in A \}\)】
cvt …【\(a \, {\mathop{{\sf f}}} \, B\)】≃【\(\{ a \mathop{{\sf f}} b \mid b \in B \}\)】
cvt …【\(A \, {\mathop{{\sf f}}} \, B\)】≃【\(\{ a \mathop{{\sf f}} b \mid a \in A , b \in B \}\)】
Pを+に？#Pは#+に？
a3
クラスが集合であるかは注意を要する問題です。クラスの中で集合でないものは固有クラスと呼ばれます。\(\dagger\)
集合となるクラス
word(c,p) … \(\dot\exists\)Exi.【\(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)】
Russelのパラドクスが固有クラスの最初の例を与えます。
word(,c) … \(\mathbb{V}_0\)
\V0.【\(\mathbb{V}_0 = \{ x \mid x \notin x \}\)】
【\(\neg \dot\exists \mathbb{V}_0\)】\(\blacktriangleleft\)
次のものも固有クラスです。
word(,c) … \(\mathbb{V}_1\)
\V1.'【\(\mathbb{V}_1 = \{ x \mid x \notin \bigcup x \}\)】
【\(\neg \dot\exists \mathbb{V}_1\)】\(\blacktriangleleft\)
【\(\mathbb{V}_1 \subset \mathbb{V}_0\)】\(\blacktriangleleft\)
集合の存在公理
次のZFの公理には、代わりとなるwordの定義があります。空集合公理…\0.
対集合公理…set2.
和集合公理…Cup.
べき集合公理…wp.
次の正則性公理もZFの公理に含まれます。
ax_r'【\(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)】
【\(\mathbb{V}_1 = \mathbb{V}\)】\(\blacktriangleleft\)
集合とクラスの共通部分は集合になります（分出公理）。\(\dagger\)
word(c,p) … \(\text{ax_s}\)
ax_s.【\(\text{ax_s} ( C ) \Longleftrightarrow \forall X \, \dot\exists ( X \cap C )\)】
c-Form \({\tt C}\) に対して `ax_s(\({\tt C}\))` が公理に含まれます。
【\(\neg \dot\exists \mathbb{V}\)】\(\blacktriangleleft\)
残り2つのZFの公理は後程与えられます。