2 自然数

2.1 自然数の作成

自然数は作らず、無定義語 \(\mathbb{M}\)・\(0\)・\({\rm suc}\) と、証明に必要な性質だけを公理として置きます。
word(,s) … \(\mathbb{M}\)  \(0\)
word(s,s) … \(\textit{+1}\)
𝕄0s … \(0 \in \mathbb{M} , \forall n \in \mathbb{M} . n \textit{+1} \in \mathbb{M}\)
IND𝕄 … \(0 \in C , \forall m \in \mathbb{M} . ( m \in C \Longrightarrow m \textit{+1} \in C ) \Longrightarrow \mathbb{M} \subset C\)
suc𝕄 … \(\begin{cases} n \in \mathbb{M} \Longrightarrow n \textit{+1} \neq 0 \\ m , n \in \mathbb{M} , m \textit{+1} = n \textit{+1} \Longrightarrow m = n \end{cases}\)
\(\mathbb{N}\) は 0 でない自然数の全体です。
word(,s) … \(\mathbb{N}\)
ℕ. … \(\mathbb{N} = \{ n \in \mathbb{M} \mid n \neq 0 \}\)

word(,s) … \({\tt n}\)
\({\tt n}\). … \({\tt n} = ( {\tt n\,{\text -}\,1} ) \textit{+1}\)

2.2 加法

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\) 𝕄0s ，IND𝕄 ，+𝕄
+1 … \(m \in \mathbb{M} \Longrightarrow m \textit{+1} = m + 1\) \(\blacktriangleleft\) 𝕄0s ，+𝕄 ，1.
+C … \(m , n \in \mathbb{M} \Longrightarrow m + n = n + m\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄
+A … \(m , n , k \in \mathbb{M} \Longrightarrow ( m + n ) + k = m + ( n + k )\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄

2.3 乗法

word(ss,s) … \(\cdot\)
*𝕄 … \(\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 , n \in \mathbb{M} \Longrightarrow m \cdot n \in \mathbb{M}\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
Ldist … \(m , n , k \in \mathbb{M} \Longrightarrow m \cdot ( n + k ) = m \cdot n + m \cdot k\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
⋅C … \(m , n \in \mathbb{M} \Longrightarrow m \cdot n = n \cdot m\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
⋅A … \(m , n , k \in \mathbb{M} \Longrightarrow ( m \cdot n ) \cdot k = m \cdot ( n \cdot k )\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄

2.4 冪

word(ss,s) … ↑
↑𝕄 … \(\begin{cases} m \in \mathbb{M} \Longrightarrow m ^ 0 = 1 \\ m , n \in \mathbb{M} \Longrightarrow m ^ { n \textit{+1} } = ( m ^ n ) \cdot m \end{cases}\)
↑∈𝕄 … \(m , n \in \mathbb{M} \Longrightarrow m ^ n \in \mathbb{M}\) \(\blacktriangleleft\) 𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄 ，↑𝕄 ，1.

2.5 順序

word(ss,p) … \(\le\)  \(<\)
≤. … \(m \le n \Longleftrightarrow \exists k \in \mathbb{M} . n = k + m\)
<. … \(m < n \Longleftrightarrow m \textit{+1} \le n\)
Ltot … \(m , n \in \mathbb{M} \Longrightarrow m \le n \mathbin{\rm o\!r} n < m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄
L≤R … \(n \in \mathbb{M} \Longrightarrow n \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄
L≤T … \(x , y , z \in \mathbb{M} , x \le y \le z \Longrightarrow x \le z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄

強い帰納法：\(n\) より小さいすべての数で成り立てば \(n\) でも成り立つなら、すべての自然数で成り立つ。
SIND𝕄 … \(\forall n \in \mathbb{M} . ( \forall z \in \mathbb{M} . ( z < n \Longrightarrow z \in D ) \Longrightarrow n \in D ) \Longrightarrow \mathbb{M} \subset D\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄

順序の補題（証明で使う）。
⋅K … \(x , y \in \mathbb{M} , a \in \mathbb{N} , x \cdot a = y \cdot a \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

2.6 偶数と奇数

どの自然数も偶数 \(2k\) か奇数 \(2k+1\) のどちらか一方。証明では「\(2k\) か \(2k+1\) と書ける」（Lpar）・「両方にはならない」（Lne）の形を使い、表には集合の形（𝕄偶奇）で見せます。
平方の展開：\((f+c)^2 = f^2 + 2fc + c^2\)（Sx）、\((2k)^2 = 2(2k^2)\)（Sx2k）、\((2k+1)^2 = 2(2(k^2+k)) + 1\)（Sx2k1）。
自然数は偶数全体 \(2\mathbb{M}\) と奇数全体 \(2\mathbb{M}+1\) に分かれる（𝕄偶奇）。\(b \cdot X\) は \(X\) の各元に \(b\) を掛けた集合、\(X + b\) は各元に \(b\) を足した集合。
word(ss,s) … \(\cdot\)  \(+\)
*^⋅. … \(b \cdot X = \{ b \cdot a \mid a \in X \}\)
^*+. … \(X + b = \{ a + b \mid a \in X \}\)
𝕄偶奇 … \(\mathbb{M} = 2 \cdot \mathbb{M} \cup ( 2 \cdot \mathbb{M} + 1 ) , 2 \cdot \mathbb{M} \cap ( 2 \cdot \mathbb{M} + 1 ) = \emptyset\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

2.7 整除と素数

\(d \mid n\) は \(d\) が \(n\) を割り切ること。\(\mathbb{P}\) は素数全体の集合。
word(ss,p) … \(\mid\)
∣. … \(d \mid n \Longleftrightarrow \exists k \in \mathbb{M} . n = d \cdot k\)
∣≤ … \(d \in \mathbb{M} , n \in \mathbb{N} , d \mid n \Longrightarrow d \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
∣T … \(p , d , n \in \mathbb{M} , p \mid d , d \mid n \Longrightarrow p \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
word(,s) … \(\mathbb{P}\)
ℙ. … \(\mathbb{P} = \{ p \in \mathbb{N} \mid 2 \le p , \forall d \in \mathbb{N} . ( d \mid p \Longrightarrow d = 1 \mathbin{\rm o\!r} d = p ) \}\)
\(d\) が \(b\) を割るとき、\(d\) が \(a\) を割ることと \(a + b\) を割ることは同じ（∣+・∣sub）。
∣+ … \(d , a , b \in \mathbb{M} , d \mid a , d \mid b \Longrightarrow d \mid a + b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，+𝕄 ，*𝕄
∣sub … \(d , u , v \in \mathbb{M} , d \mid u + v , d \mid u \Longrightarrow d \mid v\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄