4 自然数

4.1 記号

0以上の自然数\({\tt n}\)に対し
word(,s) … \({\tt n}\)
0. … \(0 = \emptyset\)
1以上の自然数 \({\tt n}\) に対し
\({\tt n}\). … \({\tt n} = \{ 0 , \cdots , {\tt n\,{\text -}\,1} \}\)
0=∅ … \(0 = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\)

4.2 自然数の基本公理

word(ss,s) … \(+\)
word(,s) … \(\mathbb{M}\)
後続 \(n + 1\) はノイマンの作り方 \(n \cup \{n\}\) とします。
Ax+1 … \(n \in \mathbb{M} \Longrightarrow n + 1 = n \cup \{ n \}\)
自然数の集まり \(\mathbb{M}\) は次を満たすとする。
𝕄1 … \(\forall n \in \mathbb{M} . n + 1 \in \mathbb{M}\)

\({\tt n} \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+1 ，\(0 \in \mathbb{M}\) ，𝕄1
\({\tt n}\).. … \({\tt n} = ( {\tt n\,{\text -}\,1} ) + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+1 ，\(0 \in \mathbb{M}\) ，𝕄1
2以上の自然数\({\tt n}\)に対し
∈\({\tt n}\) … \(0 \in 1 \in \cdots \in {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
≠\({\tt n}\) … \(0 \neq 1 , \cdots\!\cdots , {\tt n\,{\text -}\,2} \neq {\tt n\,{\text -}\,1}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

4.3 帰納法

帰納法の原理を仮定に置く。
INDC … \(0 \in D , \forall m \in \mathbb{M} . ( m \in D \Longrightarrow m + 1 \in D ) \Longrightarrow \mathbb{M} \subset D\)
Ax𝕄 … Ax+1 ，\(0 \in \mathbb{M}\) ，𝕄1 ，INDC
Lpred … \(k \in \mathbb{M} , k \neq 0 \Longrightarrow \exists j \in \mathbb{M} . k = j + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s
Lirr … \(n \in \mathbb{M} \Longrightarrow n \notin n , \forall x \in n . x \subset n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄

4.4 個数

1点を足すと個数が1つ増える。
LB1 … \(X \stackrel{\#}= n \in \mathbb{M} , x \notin X \Longrightarrow X \cup \{ x \} \stackrel{\#}= n + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄
1点ずつ足して個数が等しいなら、元の個数も等しい。
=#∪1 … \(X \cup \{ a \} \stackrel{\#}= Y \cup \{ b \} , a \notin X , b \notin Y \Longrightarrow X \stackrel{\#}= Y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
個数の等しい自然数は等しい。
L=#𝕄 … \(m , n \in \mathbb{M} , m \stackrel{\#}= n \Longrightarrow m = n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s
1点を除くと個数が1つ減る。
L∖1 … \(k \in \mathbb{M} , X \stackrel{\#}= k + 1 , x \in X \Longrightarrow X \mathop\setminus \{ x \} \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s

4.5 正の自然数

word(,s) … \(\mathbb{N}\)
ℕ. … \(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)
\(\lceil \bullet + 1 \rfloor | _ \mathbb{M} \in \mathbb{M} \stackrel{\rm IS}\to \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s