×と分配法則1
〇健全な研究室
天々城
「×も+と同じく、結合性や可換性がある」
ディアナ
「∧∨とよく似てますね」
エーリル
「確かに似てる」
天々城
「+×は吸収法則が成り立たないから、そこで違いがあるナ。
まずは、分配法則から倒そう」
■thm2.6(+×の左分配法則)
m,n,l:変数記号
+,×:項数2の関数記号
PA |- (∀m (∀n (∀l ((m×(n+l)) = ((m×n)+(m×l))))))
proof
1 (∀n ((n+0) = n)) [PA2]
2 ((n+0) = n) [∀el 1]
3 ((m×(n+0)) = (m×n)) [項の代入原理 2]
4 (((m×n)+0) = (m×n)) [∀el 1]
5 (∀n ((n×0) = 0)) [PA3]
6 ((m×0) = 0) [∀el 5]
7 (((m×n)+(m×0)) = ((m×n)+0)) [項の代入原理 6]
8 (((m×n)+(m×0)) = (m×n)) [=の推移性 7,4]
9 ((m×n) = ((m×n)+(m×0))) [=の可換性 8]
10 ((m×(n+0)) = ((m×n)+(m×0))) [=の推移性 3,9]
k:変数記号
11 ((m×(n+k)) = ((m×n)+(m×k))) [ax]
12 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
13 ((n+S(k)) = S((n+k))) [AAel 12]
14 ((m×(n+S(k))) = (m×S((n+k)))) [項の代入原理 13]
15 (∀m (∀n ((m×S(n)) = ((m×n)+m)))) [PA5]
16 ((m×S((n+k))) = ((m×(n+k))+m)) [AAel 15]
17 (((m×(n+k))+m) = (((m×n)+(m×k))+m)) [項の代入原理 11]
18 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [+の結合性]
19 ((((m×n)+(m×k))+m) = ((m×n)+((m×k)+m))) [AAel 18]
20 ((m×S(k)) = ((m×k)+m)) [AAel 15]
21 (((m×n)+(m×S(k))) = ((m×n)+((m×k)+m))) [項の代入原理 20]
22 (((m×n)+((m×k)+m)) = ((m×n)+(m×S(k)))) [=の可換性 21]
23 ((m×(n+S(k))) = ((m×n)+(m×S(k)))) [=の5推移性 14,16,17,19,22]
24 (((m×(n+k)) = ((m×n)+(m×k)))⇒((m×(n+S(k))) = ((m×n)+(m×S(k))))) [⇒in 23 el 11]
25 (∀k (((m×(n+k)) = ((m×n)+(m×k)))⇒((m×(n+S(k))) = ((m×n)+(m×S(k)))))) [∀in 24]
26 (∀l ((m×(n+l)) = ((m×n)+(m×l)))) [数学的帰納法 10,25]
27 (∀n (∀l ((m×(n+l)) = ((m×n)+(m×l))))) [∀in 26]
28 (∀m (∀n (∀l ((m×(n+l)) = ((m×n)+(m×l)))))) [∀in 27]
■
エーリル
「左？」
天々城
「分配法則には左右があるナ。
右からかけるか、左からかけるかの違いだが、自然数では両方証明できる。
そして、×の結合性を証明するときに左分配法則があると高速で証明できる」
■thm2.7(×の結合性)
m,n,l:変数記号
×:項数2の関数記号
PA |- (∀m (∀n (∀l (((m×n)×l) = (m×(n×l))))))
proof
1 (∀n ((n×0) = 0)) [PA4]
2 (((m×n)×0) = 0) [∀el 1]
3 ((n×0) = 0) [∀el 1]
4 ((m×(n×0)) = (m×0)) [項の代入原理 3]
5 ((m×0) = 0) [∀el 1]
6 ((m×(n×0)) = 0) [=の推移性 4,5]
7 (0 = (m×(n×0))) [=の可換性 6,7]
8 (((m×n)×0) = (m×(n×0))) [=の推移性 2,7]
k:変数記号
9 (((m×n)×k) = (m×(n×k))) [ax]
10 (∀m (∀n ((m×S(n)) = ((m×n)+m)))) [PA5]
11 (((m×n)×S(k)) = (((m×n)×k)+(m×n))) [AAel 10]
12 ((((m×n)×k)+(m×n)) = ((m×(n×k))+(m×n))) [項の代入原理 9]
13 (∀m (∀n (∀l ((m×(n+l)) = ((m×n)+(m×l)))))) [+×の左分配法則]
14 ((m×((n×k)+n)) = ((m×(n×k))+(m×n))) [AAel 13]
15 (((m×(n×k))+(m×n)) = (m×((n×k)+n))) [=の可換性 14]
16 ((n×S(k)) = ((n×k)+n)) [AAel 10]
17 ((m×(n×S(k))) = (m×((n×k)+n))) [項の代入原理 1]
18 ((m×((n×k)+n)) = (m×(n×S(k)))) [=の可換性 17]
19 (((m×n)×S(k)) = (m×(n×S(k)))) [=の4推移性 11,12,15,18]
20 ((((m×n)×k) = (m×(n×k)))⇒(((m×n)×S(k)) = (m×(n×S(k))))) [⇒in 19 el 9]
21 (∀k ((((m×n)×k) = (m×(n×k)))⇒(((m×n)×S(k)) = (m×(n×S(k)))))) [∀in 20]
22 (∀l (((m×n)×l) = (m×(n×l)))) [数学的帰納法 8,21]
23 (∀n (∀l (((m×n)×l) = (m×(n×l))))) [∀in 22]
24 (∀m (∀n (∀l (((m×n)×l) = (m×(n×l)))))) [∀in 23]
■
天々城
「高速と言ったが、あまり速くなかった」
ディアナ
「数学的帰納法は証明が長くなりますね」
天々城
「数学に慣れてくると書かないからナ」
ディアナ
「私はまだ慣れてないようです」
■thm2.8(×の左吸収元)
0:定数記号
×:項数2の関数記号
PA |- (∀n ((0×n) = 0))
proof
1 (∀n ((n×0) = 0)) [PA4]
2 ((0×0) = 0) [∀el 1]
k:変数記号
3 ((0×k) = 0) [ax]
4 (∀m (∀n ((m×S(n)) = ((m×n)+m)))) [PA5]
5 ((0×S(k)) = ((0×k)+0)) [AAel 4]
6 (((0×k)+0) = (0+0)) [項の代入原理 3]
7 (∀n ((n+0) = n)) [PA2]
8 ((0+0) = 0) [∀el 7]
9 ((0×S(k)) = 0) [=の3推移性 5,6,8]
10 (((0×k) = 0)⇒((0×S(k)) = 0)) [⇒in 9 el 3]
11 (∀k (((0×k) = 0)⇒((0×S(k)) = 0))) [∀in 10]
12 (∀n ((0×n)=0)) [数学的帰納法 2,11]
■
エーリル
「+の単位元で似たようなの見た」
天々城
「0を左からかけると、どんな自然数も0になるわけだ。
PA4が右吸収元。0を右からかけると、どんな自然数も0になる」
(∀n ((n×0) = 0)) [PA4]
(∀n ((0×n) = 0)) [×の左吸収元]
エーリル
「0に圧縮された」
天々城
「問題は×の可換性だ。
+の可換性の難易度をもう一段階あげたような証明になる」
■thm2.9(×の可換性)
m,n,l:変数記号
×:項数2の関数記号
PA |- (∀m (∀n ((m×n) = (n×m))))
proof
1 (∀n ((n×0) = 0)) [PA4] @@
2 ((m×0) = 0) [∀el 1]
3 (∀n ((0×n) = 0)) [×の左吸収元]
4 ((0×m) = 0) [∀el 3]
5 (0 = (0×m)) [=の可換性 4]
6 ((m×0) = (0×m)) [=の推移性 2,5]
k:変数記号
7 ((k×0) = 0) [∀el 1]
8 (((k×0)+0) = (0+0)) [項の代入原理 7]
9 (∀n ((n+0) = n)) [PA2]
10 ((0+0) = 0) [∀el 9]
11 ((S(k)×0) = 0) [∀el 1]
12 (0 = (S(k)×0)) [=の可換性 11]
13 (((k×0)+0) = (S(k)×0)) [=の3推移性 8,10,12]
l:変数記号
14 (((k×l)+l) = (S(k)×l)) [ax]
15 (∀m (∀n ((m×S(n)) = ((m×n)+m)))) [PA5]
16 ((k×S(l)) = ((k×l)+k)) [AAel 15]
17 (((k×S(l))+S(l)) = (((k×l)+k)+S(l))) [項の代入原理 16]
18 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [+の結合性]
19 ((((k×l)+k)+S(l)) = ((k×l)+(k+S(l)))) [AAel 18]
20 (∀k (∀m ((k+S(m)) = (S(k)+m)))) [thm2.4]
21 ((k+S(l)) = (S(k)+l)) [AAel 20]
22 (∀m (∀n ((m+n) = (n+m)))) [+の可換性]
23 ((S(k)+l) = (l+S(k))) [AAel 22]
24 ((k+S(l)) = (l+S(k))) [=の推移性 21,23]
25 (((k×l)+(k+S(l))) = ((k×l)+(l+S(k)))) [項の推移性 24]
26 ((((k×l)+l)+S(k)) = ((k×l)+(l+S(k)))) [AAel 18]
27 (((k×l)+(l+S(k))) = (((k×l)+l)+S(k))) [=の可換性 26]
28 (((k×l)+l)+S(k)) = ((S(k)×l)+S(k))) [項の代入原理 14]
29 ((S(k)×S(l)) = ((S(k)×l)+S(k))) [AAel 15]
30 (((S(k)×l)+S(k)) = (S(k)×S(l))) [=の可換性 ]
31 (((k×S(l))+S(l)) = (S(k)×S(l))) [=の6推移性 17,19,25,27,28,30]
32 ((((k×l)+l) = (S(k)×l))⇒(((k×S(l))+S(l)) = (S(k)×S(l)))) [⇒el 31 el 14]
33 (∀l ((((k×l)+l) = (S(k)×l))⇒(((k×S(l))+S(l)) = (S(k)×S(l))))) [∀in 32]
34 (∀m (((k×m)+m) = (S(k)×m))) [数学的帰納法 13,33]
35 ((m×k) = (k×m)) [ax]
36 ((m×S(k)) = ((m×k)+m)) [AAel 15]
37 (((m×k)+m) = ((k×m)+m)) [項の代入原理 35]
38 (((k×m)+m) = (S(k)×m)) [∀el 34]
39 ((m×S(k)) = (S(k)×m)) [=の3推移性36,37,38]
40 (((m×k) = (k×m))⇒((m×S(k)) = (S(k)×m))) [⇒in 39 el 35]
41 (∀k (((m×k) = (k×m))⇒((m×S(k)) = (S(k)×m)))) [∀in 40]
42 (∀n ((m×n) = (n×m))) [数学的帰納法 6,41]
43 (∀m (∀n ((m×n) = (n×m)))) [∀in 42]
■
天々城
「証明の中盤は+の性質を駆使した感じだナ」
エーリル
「×も魔境だ……」
