順序対およびその使用についての基本諸事項を整備します。<a href="javascript:void(0);" onclick="js_alert('順序対の定義もされません。順序対については ={x,{x,y}} という定義がされることもありますが、たぶんその定義は役に立ちません。なお1-cで「順序対」と表記が同じになる「列」が作られます。')">(dagger)
最初の使用例として、置換公理の簡潔な記述を与えます。その後に分出公理も与えます。(dagger)
順序対の集合は関係と呼ばれ、写像が特別な関係として定義されます。(dagger)
\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
\(\mathbb{W}_0\)(,s) … \(\emptyset\)
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\0.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
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} \}\)
cup_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)
cap_. … \(A \cap B = \{ x \mid x \in A , x \in B \}\)
dif_. … \(A \setminus B = \{ x \mid x \in A , x \notin B \}\)
\(\mathbb{W}_1\)(c,c) … \(\mathop\setminus\)
xs. … \(\mathop\setminus Y = \{ x \mid x \notin Y \}\)
\(\mathbb{W}_0\)(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
cup. … \({\cup} \stackrel{\star\!\star}{=} {\cup}\)
cap. … \({\cap} \stackrel{\star\!\star}{=} {\cap}\)
dif. … \({\mathop\setminus} \stackrel{\star\!\star}{=} {\setminus}\)
\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
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\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s,s)R … \(\bigcup\) \(\bigcap\)
Cup. … \({\bigcup} \stackrel{\star}{=} {\bigcup}\)
Cap. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{1}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} x \in X\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{i}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} ( \mathbin{{\sf f}} x ) = x\)
\(( X , { \mathbin{f} } ) :\underline{1} \Longleftrightarrow \stackrel{\text{^}}{\mathbin{f}} X \subset X\)
\(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( X , { [ \bullet ] } ) :\underline{1}\&\mathsf{i}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
$X {^^}$..f $X sub_ $X としたいが…？
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{I}\) ≃ \(\forall x \in X . x \mathbin{{\sf f}} x = x\)
\(\mathbb{W}_2\)(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , {\mathbin{{\sf f}}} )\) ≃ \(\{ e \mid \forall x \in X . e \mathbin{{\sf f}} x = x = x \mathbin{{\sf f}} e \}\)
wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( \wp X , {\cup} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( \wp X , {\cap} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \in \text{unit} ( \wp X , {\cup} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \in \text{unit} ( \wp X , {\cap} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
\(\mathbb{W}_0\)(s,s) … \(\triangleleft\) \(\triangleright\)
pr<. … \(\triangleleft \langle x , y \rangle = x\)
pr>. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
\(\mathbb{W}_1\)(,c) … \(\mathbb{V}_0\)
\V0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O
ax0 … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
\(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax0
*^ap_. … \(R ( X ) = \{ y \mid \exists x \in X . \langle x , y \rangle \in R \}\)
\(\mathbb{W}_1\)(c,c)F … \({!_\triangleleft}\)
pr<!. … \({!_\triangleleft} ( R ) = \{ x \mid \, ! y \, \langle x , y \rangle \in R \}\)
\(\mathbb{W}_1\)(c,p) … \(\text{ax_r}\)
ax_r. … \(\text{ax_r} ( R ) \Longleftrightarrow \forall X \subset {!_\triangleleft} ( R ) . \dot\exists R ( X )\)
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.
Le_set2 … \(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) wp. ，sub. ，\0.
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) Ax_r ，Le_set2 ，pr:0
ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \exists X \, C \subset X \Rightarrow \dot\exists C\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) Ax_s
\(C \subset X \Rightarrow \dot\exists C\) \(\blacktriangleleft\) Ax_r ，pr:0
Thm査読
最初の使用例として、置換公理の簡潔な記述を与えます。その後に分出公理も与えます。(dagger)
順序対の集合は関係と呼ばれ、写像が特別な関係として定義されます。(dagger)
a
宇宙、空集合
\(\mathbb{W}_1\)(,c) … \(\mathbb{V}\)\V. … \(\mathbb{V} = \{ x \mid \top \}\)
\(x \in \mathbb{V}\) \(\blacktriangleleft\) O
\(X \subset \mathbb{V}\) \(\blacktriangleleft\) O
\(\mathbb{W}_0\)(,s) … \(\emptyset\)
\0. … \(\emptyset = \{ x \mid {\perp} \}\)
\(x \notin \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \subset X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\0.. … \(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
有限集合
1以上の自然数 \({\tt n}\) に対して\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
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} \}\)
合併、共通部分、差
\(\mathbb{W}_1\)(cc,c) … \(\cup\) \(\cap\) \(\setminus\)cup_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)
cap_. … \(A \cap B = \{ x \mid x \in A , x \in B \}\)
dif_. … \(A \setminus B = \{ x \mid x \in A , x \notin B \}\)
\(\mathbb{W}_1\)(c,c) … \(\mathop\setminus\)
xs. … \(\mathop\setminus Y = \{ x \mid x \notin Y \}\)
\(\mathbb{W}_0\)(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
cup. … \({\cup} \stackrel{\star\!\star}{=} {\cup}\)
cap. … \({\cap} \stackrel{\star\!\star}{=} {\cap}\)
dif. … \({\mathop\setminus} \stackrel{\star\!\star}{=} {\setminus}\)
\(X \mathop\setminus Y = X \cap ( \mathop\setminus Y )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \subset Y \Longleftrightarrow X \cup Y = Y \Longleftrightarrow X \cap Y = X\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
総合併、総共通部分
\(\mathbb{W}_1\)(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\) \(\mathbb{W}_0.\)
\(\mathbb{W}_0\)(s,s)R … \(\bigcup\) \(\bigcap\)
Cup. … \({\bigcup} \stackrel{\star}{=} {\bigcup}\)
Cap. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
\(X = \bigcup \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X = \bigcap \{ X \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cup Y = \bigcup \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X = \bigcup _{ x \in X } \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
b
1項関数の1項述語
\(\mathbb{W}_2\)(s[s,s],p)R … \(:\underline{1}\) \(:\mathsf{i}\)lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{1}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} x \in X\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{i}\) ≃ \(\forall x \in X . \mathbin{{\sf f}} ( \mathbin{{\sf f}} x ) = x\)
\(( X , { \mathbin{f} } ) :\underline{1} \Longleftrightarrow \stackrel{\text{^}}{\mathbin{f}} X \subset X\)
\(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( X , { [ \bullet ] } ) :\underline{1}\&\mathsf{i}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
2項関数の1項述語
\(\mathbb{W}_2\)(s[ss,s],p)R … \(:\underline{2}\) \(:\mathsf{C}\) \(:\mathsf{A}\) \(:\mathsf{I}\)lower … \(( X , {\mathbin{{\sf f}}} ) :\underline{2}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y \in X\)
$X {^^}$..f $X sub_ $X としたいが…？
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{C}\) ≃ \(\forall x , y \in X . x \mathbin{{\sf f}} y = y \mathbin{{\sf f}} x\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{A}\) ≃ \(\forall x , y , z \in X . x \mathbin{{\sf f}} \, ( y \mathbin{{\sf f}} z ) = ( x \mathbin{{\sf f}} y ) \mathbin{{\sf f}} z\)
lower … \(( X , {\mathbin{{\sf f}}} ) :\mathsf{I}\) ≃ \(\forall x \in X . x \mathbin{{\sf f}} x = x\)
\(\mathbb{W}_2\)(s[ss,s],c) … \(\text{unit}\)
lower … \(\text{unit} ( X , {\mathbin{{\sf f}}} )\) ≃ \(\{ e \mid \forall x \in X . e \mathbin{{\sf f}} x = x = x \mathbin{{\sf f}} e \}\)
べき集合
\(\mathbb{W}_0\)(s,s) … \(\wp\)wp. … \(\wp X = \{ A \mid A \subset X \}\)
wp0 … \(\wp \emptyset = \{ \emptyset \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
wp1 … \(\wp \{ x \} = \{ \emptyset , \{ x \} \}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( \wp X , {\cup} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(( \wp X , {\cap} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\&\mathsf{I}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(\emptyset \in \text{unit} ( \wp X , {\cup} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
\(X \in \text{unit} ( \wp X , {\cap} )\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
c
順序対
\(\mathbb{W}_0\)(ss,s)F … \(\mathsf{pr}\)abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
\(\mathbb{W}_0\)(s,s) … \(\triangleleft\) \(\triangleright\)
pr<. … \(\triangleleft \langle x , y \rangle = x\)
pr>. … \(\triangleright \langle x , y \rangle = y\)
pr:0 … \(\langle x_{0} , y_{0} \rangle = \langle x_{1} , y_{1} \rangle \Longleftrightarrow x_{0} = x_{1} , y_{0} = y_{1}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\)
集合となるクラス、正則性公理
\(\mathbb{W}_1\)(c,p) … \(\dot\exists\)Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
\(\mathbb{W}_1\)(,c) … \(\mathbb{V}_0\)
\V0. … \(\mathbb{V}_0 = \{ x \mid x \notin x \}\)
\(\neg \dot\exists \mathbb{V}_0\) \(\blacktriangleleft\) O
ax0 … \(\forall X \neq \emptyset . \exists Y \in X . X \cap Y = \emptyset\)
\(\mathbb{V}_0 = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}_0.\) ，ax0
置換公理
\(\mathbb{W}_1\)(cc,c) … *^ap_*^ap_. … \(R ( X ) = \{ y \mid \exists x \in X . \langle x , y \rangle \in R \}\)
\(\mathbb{W}_1\)(c,c)F … \({!_\triangleleft}\)
pr<!. … \({!_\triangleleft} ( R ) = \{ x \mid \, ! y \, \langle x , y \rangle \in R \}\)
\(\mathbb{W}_1\)(c,p) … \(\text{ax_r}\)
ax_r. … \(\text{ax_r} ( R ) \Longleftrightarrow \forall X \subset {!_\triangleleft} ( R ) . \dot\exists R ( X )\)
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) set2.
Le_set2 … \(\exists C \, \exists^* s , t ( s , t \in C )\) \(\blacktriangleleft\) wp. ，sub. ，\0.
\(\dot\exists \{ a \mid a = x \mathbin{\rm o\!r} a = y \}\) \(\blacktriangleleft\) Ax_r ，Le_set2 ，pr:0
分出公理
\(\mathbb{W}_1\)(c,p) … \(\text{ax_s}\)ax_s. … \(\text{ax_s} ( C ) \Longleftrightarrow \exists X \, C \subset X \Rightarrow \dot\exists C\)
\(\neg \dot\exists \mathbb{V}\) \(\blacktriangleleft\) Ax_s
\(C \subset X \Rightarrow \dot\exists C\) \(\blacktriangleleft\) Ax_r ，pr:0
Thm査読