book プレビュー

自然数の公理と算術

import 0.book

自然数を公理で与える本が共通に使う準備。

1 自然数の公理

\(m^n\) は \(m\) の \(n\) 乗（ソースでは m ↑ n）。↑𝕄 の漸化式を満たす演算として仮定します（存在は示しません）。
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.

\(m \le n\) は \(n = k + m\) となる \(k \in \mathbb{M}\) があること。\(m < n\) は \(m+1 \le n\)。
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 , 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 , a \in \mathbb{M} , a \neq 0 , x \cdot a = y \cdot a \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

どの自然数も偶数 \(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 \}\)
word(ss,s) … \(\cup\) \(\cap\)
∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
∩. … \(X \cap Y = \{ x \mid x \in X , x \in Y \}\)
word(,s) … \(\emptyset\)
∅. … \(\emptyset = \{ x \mid {\perp} \}\)
𝕄偶奇 … \(\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𝕄 ，+𝕄 ，*𝕄

\(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 , n \in \mathbb{M} , d \mid n , n \neq 0 \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{M} \mid 2 \le p , \forall d \in \mathbb{M} . ( 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𝕄 ，+𝕄 ，*𝕄