2 自然数
2.1 0と後続関数
word(,s) …
\(0\)0. …
\(0 = \emptyset\) word(s,s) …
\(\textit{+1}\) \(\hat{\textit{+1}}\)suc. …
\(n \textit{+1} = n \cup \{ n \}\) ^suc. …
\(X \hat{\textit{+1}} = \{ x \textit{+1} \mid x \in X \}\) 2.2 帰納法
word(c,c) …
\(\bigcap\)⋂_. …
\(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\) word(,c) …
\(\text{Ind}\)Ind. …
\(\text{Ind} = \{ M \mid 0 \in M , M \hat{\textit{+1}} \subset M \}\) word(,s) …
\(\mathbb{M}\)𝕄. …
\(\mathbb{M} = \bigcap \text{Ind}\) 𝕄 は集合の語なので、𝕄. は \(\bigcap {\rm Ind}\) が集合であること＝無限公理に当たる内容を含みます。
\(\mathbb{M} \in \text{Ind}\) \(\blacktriangleleft\) \(\mathbb{W}.\)Lirr …
\(n \in \mathbb{M} \Longrightarrow n \notin n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s2.3 自然数の記号
word(,s) …
\({\tt n}\)\({\tt n}\). …
\({\tt n} = \{ 0 , \cdots , {\tt n\,{\text -}\,1} \}\) \({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\)2.4 自然数の演算
word(ss,s) …
\(+\)+𝕄 …
\(\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 , n \in \mathbb{M} \Longrightarrow m + n \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄+1 …
\(m \in \mathbb{M} \Longrightarrow m \textit{+1} = m + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，+𝕄1点を足すと個数は1つ増える（Ladd）。\(n \notin B\) なら \(B \mapsto B \cup \{n\}\) は単射で、\(n\) を含む \(n+1\) の部分集合はこの形（LJ2・LB）。
\(m + n\) は、\(m\) 個と \(n\) 個を印 \(c \neq d\) で区別して並べた集合 \(\{c\} \times m \cup \{d\} \times n\) の個数。
+=#g …
\(c \neq d , m , n \in \mathbb{M} \Longrightarrow m + n \stackrel{\#}= \{ c \} \times m \cup \{ d \} \times n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄交わらない \(m\) 個と \(k\) 個を合わせると \(m + k\) 個。
∪=#+ …
\(X \cap Y = \emptyset , m , k \in \mathbb{M} , X \stackrel{\#}= m , Y \stackrel{\#}= k \Longrightarrow X \cup Y \stackrel{\#}= m + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄