表示調整
閉じる
挿絵表示切替ボタン
▼配色
▼行間
▼文字サイズ
▼メニューバー
×閉じる

ブックマークに追加しました

設定
0/400
設定を保存しました
エラーが発生しました
※文字以内
ブックマークを解除しました。

エラーが発生しました。

エラーの原因がわからない場合はヘルプセンターをご確認ください。

ブックマーク機能を使うにはログインしてください。
45/51

×と分配法則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]



天々城

「証明の中盤は+の性質を駆使した感じだナ」


エーリル

「×も魔境だ……」

評価をするにはログインしてください。
ブックマークに追加
ブックマーク機能を使うにはログインしてください。
― 新着の感想 ―
このエピソードに感想はまだ書かれていません。
感想一覧
+注意+

特に記載なき場合、掲載されている作品はすべてフィクションであり実在の人物・団体等とは一切関係ありません。
特に記載なき場合、掲載されている作品の著作権は作者にあります(一部作品除く)。
作者以外の方による作品の引用を超える無断転載は禁止しており、行った場合、著作権法の違反となります。

この作品はリンクフリーです。ご自由にリンク(紹介)してください。
この作品はスマートフォン対応です。スマートフォンかパソコンかを自動で判別し、適切なページを表示します。

↑ページトップへ