×と分配法則2
〇健全な研究室
天々城
「+と×の可換性が証明できたのは正直デカい。
文字を入れ替えるだけで証明できるのがあるからナ」
ディアナ
「例えばどんな定理ですか？」
天々城
「そうだナ。とりあえず『1』を定義しよう」
■1の定義
1:=S(0)
エーリル
「0の次か」
ディアナ
「1だけを定義するなら、他の数も一緒に定義すればいいと思うのですが」
天々城
「0と1は自然数の中でかなり特別な数だからだ。
0は+の単位元で、×の吸収元。
そして1は×の単位元になる」
■thm2.10(×の右単位元)
PA |- (∀n ((n×1) = n))
proof
1 (1 = S(0)) [1の定義]
2 ((n×1) = (n×S(0))) [項の代入原理 1]
3 (∀m (∀n ((m×S(n)) = ((m×n)+m)))) [PA5]
4 ((n×S(0)) = ((n×0)+n)) [AAel 3]
5 (∀n ((n×0) = 0)) [PA4]
6 ((n×0) = 0) [∀el 5]
7 (((n×0)+n) = (0+n)) [項の代入原理 6]
8 (∀n ((0+n) = n)) [+の左単位元]
9 ((0+n) = n) [∀el 8]
10 ((n×1) = n) [=の4推移性 2,4,7,9]
11 (∀n ((n×1) = n)) [∀in 10]
■
■thm2.11(×の左単位元)
n:変数記号
×:項数2の関数記号
PA |- (∀n ((1×n) = n))
proof
1 (∀n ((n×1) = n)) [×の右単位元]
2 ((n×1) = n) [∀el 1]
3 (∀m (∀n ((m×n) = (n×m)))) [×の可換性]
4 ((n×1) = (1×n)) [AAel 3]
5 ((1×n) = (n×1)) [=の可換性 4]
6 ((1×n) = n) [=の推移性 5,2]
7 (∀n ((1×n) = n)) [∀in 6]
■
エーリル
「×の可換性が火を噴いた」
ディアナ
「数学的帰納法を使いませんでしたね」
天々城
「おかげで証明も半分くらいで済んでいるナ。
スキルを揃えたらあとは発動するだけって感じだ」
ディアナ
「道具が揃えば便利になるということでしょうかね」
天々城
「まあ、数学に限った話じゃないけどナ」
■thm2.12(+×の右分配法則)
m,n,l:変数記号
+,×:項数2の関数記号
PA |- (∀m (∀n (∀l (((m+n)×l) = ((m×l)+(n×l))))))
proof
1 (∀m (∀n ((m×n) = (n×m)))) [×の可換性]
2 (((m+n)×l) = ((l×(m+n))) [AAel 1]
3 (∀m (∀n (∀l ((m×(n+l)) = ((m×n)+(m×l)))))) [+×の左分配法則]
4 ((l×(m+n)) = ((l×m)+(l×n))) [AAel 3]
5 ((l×m) = (m×l)) [AAel 1]
6 ((l×n) = (n×l)) [AAel 1]
7 (((l×m)+(l×n)) = ((m×l)+(n×l))) [項の代入原理 5,6]
8 (((m+n)×l) = ((m×l)+(n×l))) [=の3推移性 2,4,7]
9 (∀l (((m+n)×l) = ((m×l)+(n×l)))) [∀in 8]
10 (∀n (∀l (((m+n)×l) = ((m×l)+(n×l))))) [∀in 9]
11 (∀m (∀n (∀l (((m+n)×l) = ((m×l)+(n×l)))))) [∀in 10]
■
天々城
「分配法則もこのくらいの変形で倒せる」
ディアナ
「可換性すごいですね」
天々城
「可換性はいいぞ」
■thm2.13(+の右簡約律)
m,n,l:変数記号
+:項数2の関数記号
PA |- (∀m (∀n (∀l (((m+l) = (n+l))⇒(m = n)))))
proof
1 ((m+0) = (n+0)) [ax]
2 (∀n ((n+0) = n)) [PA2]
3 ((m+0) = m) [∀el 2]
4 ((n+0) = n) [∀el 2]
5 (((m+0) = (n+0)) ⇔ (m = n)) [論理式の代入原理 3,4]
6 (m = n) [⇔elL 1,5]
7 (((m+0) = (n+0))⇒(m = n)) [⇒in 6,1]
k:変数記号
8 (((m+k) = (n+k))⇒(m = n)) [ax]
9 ((m+S(k)) = (n+S(k))) [ax]
10 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
11 ((m+S(k)) = S((m+k))) [AAel 10]
12 ((n+S(k)) = S((n+k))) [AAel 10]
13 (((m+S(k)) = (n+S(k))) ⇔ (S((m+k)) = S((n+k)))) [論理式の代入原理 11,12]
14 (S((m+k)) = S((n+k))) [⇔elL 9,13]
15 (∀m (∀n ((S(m) = S(n))⇒(m = n)))) [PA0]
16 ((S((m+k)) = S((n+k)))⇒((m+k) = (n+k))) [AAel 15]
17 ((S((m+k)) = S((n+k)))⇒(m = n)) [⇒の推移性 16,8]
18 (m = n) [⇒el 14,17]
19 (((m+S(k)) = (n+S(k)))⇒(m = n)) [⇒in 18 el 9]
20 ((((m+k) = (n+k))⇒(m = n)) ⇒ (((m+S(k)) = (n+S(k)))⇒(m = n))) [⇒in 19 el 8]
21 (∀k ((((m+k) = (n+k))⇒(m = n)) ⇒ (((m+S(k)) = (n+S(k)))⇒(m = n)))) [∀in 20]
22 (∀l (((m+l) = (n+l))⇒(m = n))) [数学的帰納法 7,21]
23 (∀n (∀l (((m+l) = (n+l))⇒(m = n)))) [∀in 22]
24 (∀m (∀n (∀l (((m+l) = (n+l))⇒(m = n))))) [∀in 23]
■
天々城
「同じものを足して、しかも等しいなら元の数も一緒って感じだろうナ」
エーリル
「(n+1)と(1+1)が等しいと(n = 1)か、ふむふむ」
ディアナ
「足したときに条件が揃えば『戻せる』ということですか？」
天々城
「いきなり核心をついてくるとは、さすがドワーフの姫」
■thm2.14(+の左簡約律)
m,n,l:変数記号
+:項数2の関数記号
PA |- (∀m (∀n (∀l (((l+m) = (l+n))⇒(m = n)))))
proof
1 (∀m (∀n ((m+n) = (n+m)))) [+の可換性]
2 ((m+l) = (l+m)) [AAel 1]
3 ((l+m) = (l+n)) [ax]
4 ((l+n) = (n+l)) [AAel 1]
5 ((m+l) = (n+l)) [=の3推移性 2,3,4]
6 (∀m (∀n (∀l (((m+l) = (n+l))⇒(m = n))))) [+の右簡約律]
7 (((m+l) = (n+l))⇒(m = n)) [AAel 6]
8 (m = n) [⇒el 5,7]
9 (((l+m) = (l+n))⇒(m = n)) [⇒in 8 el 3]
10 (∀l (((l+m) = (l+n))⇒(m = n))) [∀in 9]
11 (∀n (∀l (((l+m) = (l+n))⇒(m = n)))) [∀in 10]
12 (∀m (∀n (∀l (((l+m) = (l+n))⇒(m = n))))) [∀in 11]
■
エーリル
「可換性は最強」
天々城
「数学の中でも『可換』『有限』『線形』『ハウスドルフ』あたりはかなり穏やかな性格をしてるナ、。
これが『非可換』『無限』『非線形』『非ハウスドルフ』とかなるとラスボスなのに四天王になる」
エーリル
「ラストとは一体」
クアトロドルフ
「響きだけでも恐ろしいね。
人の人生を崩壊させかねないよ」
さトぅー
「無限生成非可換群を分類せよとか？」
天々城
「やめてさしあげろ」
