1 - b1
具体的な集合・クラスの作成に取りかかります。
宇宙、空集合
word(,c) … \(\mathbb{V}\)def …【\(\mathbb{V}\)】≃【\(\{ x \mid \top \}\)】
【\(x \in \mathbb{V}\)】\(\,{\blacktriangleleft}\,\)
【\(X \subset \mathbb{V}\)】\(\,{\blacktriangleleft}\,\)
word(,s) … \(\emptyset\)
\({\emptyset.}\)【\(\emptyset = \{ x \mid {\perp} \}\)】
【\(x \notin \emptyset\)】\(\,{\blacktriangleleft}\,\)
【\(\emptyset \subset X\)】\(\,{\blacktriangleleft}\,\)
\(\emptyset{.}{.}\)【\(x = \emptyset \Longleftrightarrow \not\exists y \, ( y \in x )\)】\(\,{\blacktriangleleft}\,\)
合併、共通部分、差
word(cc,c) … \(\cup\) \(\cap\)def …【\({\sf X} \cup {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} \mathbin{\rm o\!r} {\sf x} \in {\sf Y} \}\)】
def …【\({\sf X} \cap {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \in {\sf X} , {\sf x} \in {\sf Y} \}\)】
word(c,c) … \(\mathop\setminus\)
def …【\(\mathop\setminus {\sf Y}\)】≃【\(\{ {\sf x} \mid {\sf x} \notin {\sf Y} \}\)】
word(ss,s) … \(\cup\) \(\cap\) \(\mathop\setminus\)
\(\cup.\)【\(\cup \,^{\star\!\star}{=}\; \cup\)】
\(\cap.\)【\(\cap \,^{\star\!\star}{=}\; \cap\)】
\(\setminus.\)【\(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\)def …【\(\bigcup {\sf X}\)】≃【\(\{ {\sf t} \mid \exists {\sf x} \in {\sf X} . {\sf t} \in {\sf x} \}\)】
def …【\(\bigcap {\sf X}\)】≃【\(\{ {\sf t} \mid \forall {\sf x} \in {\sf X} . {\sf t} \in {\sf x} \}\)】
【\(\bigcap \emptyset = \mathbb{V}\)】\(\,{\blacktriangleleft}\,\)
word(s,s) … \(\bigcup\) \(\bigcap\)
\(\bigcup.\)【\(\bigcup \,^\star{=}\; \bigcup\)】
\(\bigcap.\)【\(X \neq \emptyset \Longrightarrow \bigcap X = \bigcap X\)】\(\,{\triangleleft}\,\)
【\(X = \bigcup \{ X \}\)】\(\,{\blacktriangleleft}\,\)
【\(X = \bigcap \{ X \}\)】\(\,{\blacktriangleleft}\,\)
【\(X \cup Y = \bigcup \{ X , Y \}\)】\(\,{\blacktriangleleft}\,\)
【\(X \cap Y = \bigcap \{ X , Y \}\)】\(\,{\blacktriangleleft}\,\)
集合は１点集合により分割されます。この教科書で、証明にsosが必要な最初の例です。
【\(X = \bigcup _{ x \in X } \{ x \}\)】\(\,{\blacktriangleleft}\,\)
集合となるクラス
word(c,p) … \(\dot\exists\)def …【\(\dot\exists {\sf X}\)】≃【\(\exists {\sf x} \, ( {\sf x} = {\sf X} )\)】
Russelのパラドクスが固有クラス(集合でないクラス)の最初の例を与えます。
word(,c) … \(\mathbb{U}_0\)
def …【\(\mathbb{U}_0\)】≃【\(\{ x \mid x \notin x \}\)】
【\(\neg \dot\exists \mathbb{U}_0\)】\(\,{\blacktriangleleft}\,\)
次のものも固有クラスです。
word(,c) … \(\mathbb{U}_1\)
def …【\(\mathbb{U}_1\)】≃【\(\{ x \mid x \notin \bigcup x \}\)】
【\(\neg \dot\exists \mathbb{U}_1\)】\(\,{\blacktriangleleft}\,\)
【\(\mathbb{U}_1 \subset \mathbb{U}_0\)】\(\,{\blacktriangleleft}\,\)
集合の存在公理
通常、公理的集合論では集合の存在に関する公理が置かれます。
当システムでは、例えば空集合公理の代わりに \(\emptyset\) と \({\emptyset.}\) を置きます。
集合とクラスの共通部分は集合になります(分出公理)が、word(sc,s)は使用できません。
無限個の公理が必要なのは頭の痛い所です。
word(c,p) … \(\text{ax_s}\)
def …【\(\text{ax_s} ( {\sf X} )\)】≃【\(\forall {\sf d} \, \dot\exists ( {\sf d} \cap {\sf X} )\)】
\(\text{ax_s}({\tt C})\) (\({\tt C}\)はc-Form) という形の全てのPropは公理に含まれます。
【\(\neg \dot\exists \mathbb{V}\)】\(\,{\blacktriangleleft}\,\)
1 - b2
自然数を作ります。帰納法が強力な道具になりますが、メタの帰納法も使われます。
自然数
word(,s) … \(0\)\({0.}\)【\(0 = \emptyset\)】\(\,{\triangleleft}\,\)
0以上の自然数全体を作ってしまいます。
word(,s) … \(\mathbb{M}\)
\(【0 \in \mathbb{M}】\)というPropがしばしば証明で使用されます。
後置される後続関数を準備します。
word(s,s) … \(\textit{+1}\) \(\textit{+1}\)
\({+}{\textit 1}.\)【\(n \textit{+1} = n \cup \{ n \}\)】\(\,{\triangleleft}\,\)
\(\textit{+1}\_.\)【\(\textit{+1} \, \,^\star{=}\; \, {\textit{+1}}\)】
帰納法
def …【\(\text{Ind}\)】≃【\(\{ M \mid 0 \in M , M \textit{+1} \subset M \}\)】帰納法を使うときだけは自然数全体として \Mi ≅ \M を使用します。
\(\mathbb{M}.\)【\(\mathbb{M} = \bigcap \text{Ind}\)】
\(\mathbb{M}1\)【\(\mathbb{M} \textit{+1} \subset \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
【\(\bigcup \mathbb{M} = \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
\({<_\mathbb{M}}0\)【\( m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\)】
\({<_\mathbb{M}}1\)【\( m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\)】\(\,{\blacktriangleleft}\,\)
【\(\mathbb{M} \subset \mathbb{U}_1\)】\(\,{\blacktriangleleft}\,\)
\(\bigcup\) が先行関数になります。
【\(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\)】\(\,{\blacktriangleleft}\,\)
\(\mathbb{M}\)が全順序であることも示します。
\(\mathbb{M}\text{D}\)【\( m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\)】\(\,{\blacktriangleleft}\,\)
準備 \(M_d.\)【\(M_d = \{ n \in \mathbb{M} \mid \forall m \in \mathbb{M} . m \subset n \mathbin{\rm o\!r} n \subset m \}\)】
新wordの準備もやりやすく
メタからの自然数の作成
1以上の自然数 \({\tt n}\) に対し word(,s) … \({\tt n}\)私たちは十進法を使用するので、「1以上の自然数」とは「1～9で始まる0～9の列」です。
自然数を集合と思う時にはvon Neumann流の定義を採用します。
\({\tt n}.\)【\({\tt n} = \{ 0 , 1 , \cdots , {\tt n\,{\text -}\,1} \}\)】\(\)
\({\tt n}{.}{.}\)【\({\tt n} = {\tt n\,{\text -}\,1} \textit{+1}\)】\(\,{\blacktriangleleft}\,\)
次のThmは \({\tt n}\geq0\) のメタ帰納法で示されます。
【\({\tt n} \in \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
2以上の自然数 \({\tt n}\) に対しては、次の長いFormを準備します。
\(\text{subn}({\tt n})\)【\(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\)】
\(\text{neq}({\tt n})\)【\(0 \neq 1 , 0 \neq 2 , \cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\)】
1以上の自然数
word(,s) … \(\mathbb{N}\)\(\mathbb{N}.\)【\(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)】\(\,{\triangleleft}\,\)
\(\mathbb{N}{.}{.}\)【\(\mathbb{N} = \mathbb{M} \textit{+1}\)】\(\,{\blacktriangleleft}\,\)
準備 \(M_n.\)【\(M_n = \{ n \in \mathbb{M} \mid n \neq 0 \Rightarrow \exists k \in \mathbb{M} . n = k \textit{+1} \}\)】
この定理はいらない気が…
1 - b3
自然数の加法
word(ss,s) … \(+\) \(+\) \(+\) \(+\)\({+}\text{l}.\)【\(+ \,^{\star\!\star}{=}\; {+}\)】 \({+}\text{r}.\)【\(+ \,^{\star\!\star}{=}\; {+}\)】 \({+}\text{_}.\)【\(+ \,^{\star\!\star}{=}\; {+}\)】
【\(\{ 0 , 1 \} + 2 = \{ 2 , 3 \}\)】となるべきです。
\({+}_\mathbb{M}\)【\(\begin{cases} m \in \mathbb{M} \Longrightarrow m + 0 = m \\ m , n \in \mathbb{M} \Longrightarrow m + ( n \textit{+1} ) = ( m + n ) \textit{+1} \end{cases}\)】
【\(m \in \mathbb{M} \Longrightarrow m + 1 = m \textit{+1}\)】\(\,{\blacktriangleleft}\,\)
【\(n \in \mathbb{M} \Longrightarrow 0 + n = n\)】\(\,{\blacktriangleleft}\,\)
準備 \(M_u.\)【\(M_u = \{ n \in \mathbb{M} \mid 0 + n = n \}\)】
\(+_\mathbb{M}0\)【\(\mathbb{M} + \mathbb{M} \subset \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
【\( m , n \in \mathbb{M} \Longrightarrow m + n = n + m\)】
【\( m , n , \in \mathbb{M} \Longrightarrow m + ( n + k ) = ( n + m ) + k\)】
0+n=n、可換則、結合則なんかは濃度を使って証明した方が良い？
自然数の乗法
word(ss,s) … \(\cdot\) \(\cdot\) \(\cdot\) \(\cdot\)\({*}\text{l}.\)【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】 \({*}\text{r}.\)【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】 \({*}\text{_}.\)【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】
【\(\{ 0 , 1 \} \cdot 2 = \{ 0 , 2 \}\)】となるべきです。
\({*}_\mathbb{M}\)【\(\begin{cases} m \in \mathbb{M} \Longrightarrow m \cdot 0 = 0 \\ m , n \in \mathbb{M} \Longrightarrow m \cdot ( n \textit{+1} ) = ( m \cdot n ) + m \end{cases}\)】
【\(n \in \mathbb{M} \Longrightarrow 0 \cdot n = 0\)】\(\,{\blacktriangleleft}\,\)
準備 \(M_q.\)【\(M_q = \{ n \in \mathbb{M} \mid 0 \cdot n = 0 \}\)】
\(*_\mathbb{M}0\)【\(\mathbb{M} \cdot \mathbb{M} \subset \mathbb{M}\)】\(\,{\blacktriangleleft}\,\)
自然数の順序
大小は加法を使って作ることもできる【\(i \in \mathbb{M} \Rightarrow \{ n \in \mathbb{M} \mid i \subset n \} = i + \mathbb{M}\)】
`i in \M => {cls n in \M | i sub n } =_ i +r \M` / +r. => ＜ Le1，M_i.，\Mi. ;; Le1 / W.-sub. ＜ `0 in \M`，\Mi1，+\M，Le2，<\M1 / subn.. ;; Le2 / W. ＜ O ;; Le1 := `i in \M => M_i(i) in_ Ind` ,, Le2 := `x sub 0 => x =s 0`
準備 \(M_i.\)【\(M_i ( i ) = \{ n \in \mathbb{M} \mid i \subset n \Rightarrow \exists m \in \mathbb{M} . n = i + m \}\)】
`i in \M => {cls n in \M | i sub n } =_ i +r \M` / W. ＜ \Mi.，Le2，M_i. ;; Le1 := `i in \M => M_i(i) in_ Ind`ダメ