b1
クラスが集合であるかは注意を要する問題になります。
クラスの中で集合でないものは固有クラスと呼ばれます。
集合となるクラス
word(c,p) … \(\dot\exists\)cvt …【\(\dot\exists C\)】≃【\(\exists X \, ( X = C )\)】
Russelのパラドクスが固有クラス(集合でないクラス)の最初の例を与えます。
word(,c) … \(\mathbb{V}_0\)
cvt …【\(\mathbb{V}_0\)】≃【\(\{ x \mid x \notin x \}\)】
【\(\neg \dot\exists \mathbb{V}_0\)】\(\blacktriangleleft\)
次のものも固有クラスです。
word(,c) … \(\mathbb{V}_1\)
cvt …【\(\mathbb{V}_1\)】≃【\(\{ x \mid x \notin \bigcup x \}\)】
【\(\neg \dot\exists \mathbb{V}_1\)】\(\blacktriangleleft\)
【\(\mathbb{V}_1 \subset \mathbb{V}_0\)】\(\blacktriangleleft\)
集合の存在公理
通常、公理的集合論では集合の存在に関する公理が置かれます。当システムでは、例えば空集合公理の代わりに \(\emptyset\) と \0. を置きます。
集合とクラスの共通部分は集合になります(分出公理)が、word(sc,s)は使用できません。
無限個の公理が必要なのは頭の痛い所です。
word(c,p) … \(\text{ax_s}\)
cvt …【\(\text{ax_s} ( C )\)】≃【\(\forall X \, \dot\exists ( X \cap C )\)】
c-Form \({\tt C}\) に対して `ax_s(\({\tt C}\))` は公理に含まれます。
【\(\neg \dot\exists \mathbb{V}\)】\(\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 \}\)】
b2
自然数を作ります。帰納法が強力な道具になりますが、メタの帰納法も使われます。
自然数
word(,s) … 00._【\(0 = \emptyset\)】
0以上の自然数全体を作ってしまいます。
word(,s) … \(\mathbb{M}\)
【\(0 \in \mathbb{M}\)】は公理になります。
後置される後続関数を準備します。
word(s,s) … \(\textit{+1}\) \(\textit{+1}\)
suc._【\(n \textit{+1} = n \cup \{ n \}\)】
suc_.【\(\textit{+1} \, \,^\star{=}\; {\textit{+1}}\)】
帰納法
cvt …【\(\text{Ind}\)】≃【\(\{ M \mid 0 \in M , M \textit{+1} \subset M \}\)】帰納法を使うときだけは自然数全体として \Mi ≅ \M を使用します。
\Mi.【\(\mathbb{M} = \bigcap \text{Ind}\)】
【\(\mathbb{M} \textit{+1} \subset \mathbb{M}\)】\(\blacktriangleleft\)
【\(\bigcup \mathbb{M} = \mathbb{M}\)】\(\blacktriangleleft\)
<\M0【\( m , n \in \mathbb{M} \Longrightarrow m \in n \Leftrightarrow m \subsetneq n\)】\(\blacktriangleleft\)
<\M1【\( m , n \in \mathbb{M} \Longrightarrow m \subsetneq n \textit{+1} \Leftrightarrow m \subset n\)】\(\blacktriangleleft\)
【\(\mathbb{M} \subset \mathbb{V}_1\)】\(\blacktriangleleft\)
\(\bigcup\) が先行関数になります。
【\(m \in \mathbb{M} \Longrightarrow \bigcup ( m \textit{+1} ) = m\)】\(\blacktriangleleft\)
\(\mathbb{M}\)が全順序であることも示します。
\MD【\( 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 \}\)】
次の注釈にあるTrainで行けるようにしたい
\MD【\( m , n \in \mathbb{M} \Longrightarrow m \subset n \mathbin{\rm o\!r} n \subset m\)】\(\blacktriangleleft\)
優先
メタからの自然数の作成
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を準備します。
in\({\tt n}\)【\(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\)】\(\blacktriangleleft\)
subn\({\tt n}\)【\(0 \subsetneq 1 \subsetneq \cdots \subsetneq {\tt n\,{\text -}\,1}\)】\(\blacktriangleleft\)
neq\({\tt n}\)【\(0 \neq 1 , 0 \neq 2 , \cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\)】
b3
自然数の加法
word(ss,s) … \(+\) \(+\) \(+\) \(+\)+l.【\(+ \,^{\star\!\star}{=}\; {+}\)】 +r.【\(+ \,^{\star\!\star}{=}\; {+}\)】 +_.【\(+ \,^{\star\!\star}{=}\; {+}\)】
【\(\{ 0 , 1 \} + 2 = \{ 2 , 3 \}\)】となるべきです。
+\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 \}\)】
+\M0_【\(\mathbb{M} + \mathbb{M} \subset \mathbb{M}\)】\(\blacktriangleleft\)
【\( m , n \in \mathbb{M} \Longrightarrow m + n = n + m\)】
【\( m , n , k \in \mathbb{M} \Longrightarrow m + ( n + k ) = ( n + m ) + k\)】
0+n=n、可換則、結合則なんかは濃度を使って証明した方が良い？
自然数の乗法
word(ss,s) … \(\cdot\) \(\cdot\) \(\cdot\) \(\cdot\)*l.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】 *r.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】 *_.【\(\cdot \,^{\star\!\star}{=}\; {\cdot}\)】
【\(\{ 0 , 1 \} \cdot 2 = \{ 0 , 2 \}\)】となるべきです。
*\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 \}\)】
*\M0_【\(\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`ダメ