自然数・整数や濃度の演算について
d1
自然数の加法
word(ss,s) … \(+\) \(+\) \(+\) \(+\)^*+. … \({+} \stackrel{\star\!\star}{=} \; \stackrel{\text{^*}}{+}\) *^+. … \({+} \stackrel{\star\!\star}{=} \; \stackrel{\text{*^}}{+}\) ^^+. … \({+} \stackrel{\star\!\star}{=} \; \stackrel{\text{^^}}{+}\)
\(\{ 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\) +\M ，1.. ，`0 in \M`
+\M:0 … \(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m + n \in \mathbb{M}\) \(\blacktriangleleft\)
+\M:0' … \(\mathbb{M} + \mathbb{M} \subset \mathbb{M}\) \(\blacktriangleleft\)
\(n \in \mathbb{M} \Longrightarrow 0 + n = n\) \(\blacktriangleleft\)
\(m , n \in \mathbb{M} \Longrightarrow m + n = n + m\)
\(m , n , k \in \mathbb{M} \Longrightarrow m + ( n + k ) = ( n + m ) + k\)
\(( \mathbb{M} , {+} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\) \(\blacktriangleleft\)
M* … \(( \mathbb{M} , {\cdot} ) :\underline{2}\&\mathsf{C}\&\mathsf{A}\)
0+n=n、可換則、結合則なんかは濃度を使って証明した方が良い？
自然数の乗法
word(ss,s) … \(\cdot\) \(\cdot\) \(\cdot\) \(\cdot\)^**. … \({\cdot} \stackrel{\star\!\star}{=} \; \stackrel{\text{^*}}{\cdot}\) *^*. … \({\cdot} \stackrel{\star\!\star}{=} \; \stackrel{\text{*^}}{\cdot}\) ^^*. … \({\cdot} \stackrel{\star\!\star}{=} \; \stackrel{\text{^^}}{\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}\)
*\M:0 … \(m \in \mathbb{M} , n \in \mathbb{M} \Longrightarrow m \cdot n \in \mathbb{M}\) \(\blacktriangleleft\)
*\M:0' … \(\mathbb{M} \cdot \mathbb{M} \subset \mathbb{M}\) \(\blacktriangleleft\)
\(n \in \mathbb{M} \Longrightarrow 0 \cdot n = 0\) \(\blacktriangleleft\)
加法・乗法の諸法則は1-dで証明されます。
自然数の順序
大小は加法を使って作ることもできる\(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 *^+ \M` / *^+. => -| Le1 ,, M_i. ,, \Mi. ;; Le1 / W.!!sub. -| `0 in \M` ,, \Mi1 ,, +\M ,, Le2 ,, <\M:1 / 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 *^+ \M` / W. -| \Mi. ,, Le2 ,, M_i. ;; Le1 := `i in \M => M_i(i) in_ Ind`ダメ
有限の計算
直和の濃度\(m , n \in \mathbb{M} \Longrightarrow ( 1 \times m ) \cup ( n \times 1 ) \stackrel{\#}= m + n\) \(\blacktriangleleft\) W.
集合の直和作る？
\(m+n = \{0\}\times m \cup \{1\}\times n\)
d2
d4
1以上の自然数
word(,s) … \(\mathbb{N}\)\N. … \(n \in \mathbb{N} \Longleftrightarrow 0 \neq n \in \mathbb{M}\) \(\blacktriangleleft\)
\N._ … \(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)
\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} \}\)
この定理はいらない気が…
整数
word(s,s) … \(-\) \(-\)^-. … \({-} \stackrel{\star}{=} \; \stackrel{\text{^}}{-}\)
suc- … \(n \in \mathbb{N} \Longrightarrow ( - n ) \textit{+1} = - ( \bigcup n )\)
word(,s) … \(\mathbb{Z}\)
整数は0以上のものと負のものに分けられるという定義を使うときは \Zm ≅ \Z を使用します。
\Zm. … \(\mathbb{Z} = \mathbb{M} \cup ( - \mathbb{N} )\)
整数の加法
+\Z … \(\begin{cases} m \in \mathbb{Z} \Longrightarrow m + 0 = m \\ m \in \mathbb{Z} , \; n \in \mathbb{M} \Longrightarrow m + ( n \textit{+1} ) = ( m + n ) \textit{+1} , m + ( - n ) = - ( - m + n ) \end{cases}\)\(+\M\)
\(m \in \mathbb{Z} \Longrightarrow m + 1 = m \textit{+1}\) \(\blacktriangleleft\) +\Z ，1.. ，`0 in \M`
\(n \in \mathbb{Z} \Longrightarrow 0 + n = n\) \(\blacktriangleleft\)
準備 M_-u. … \(M_{-u} = \{ n \in \mathbb{M} \mid 0 + ( - n ) = - n \}\)
\(0 \in \text{unit} ( \mathbb{Z} , {+} )\) \(\blacktriangleleft\)
+の性質をいろいろ？
m-nをabbrで導入すべし
整数の乗法
*\Z … \(\begin{cases} m \in \mathbb{Z} \Longrightarrow m \cdot 0 = 0 \\ m \in \mathbb{Z} , n \in \mathbb{M} \Longrightarrow m \cdot ( n \textit{+1} ) = ( m \cdot n ) + m , \; m \cdot ( - n ) = - m \cdot n \end{cases}\)*\M_unit … \(1 \in \text{unit} ( \mathbb{M} , {\cdot} )\) \(\blacktriangleleft\)
*を+より優先。precedを変える