≦
〇健全な研究室
天々城
「クワトロドルフはなにをやってるんだ？」
クアトロドルフ
「なにって、さトぅーさんから一階述語論理を教えてもらってるんだよ。
びっくりするくらい文法が多いね」
さトぅー
「自然演繹で∧∨⇔∃が最初からある体系でやってるから、文法が多いのは当たり前よ。
すぐに覚えちゃったから、あとは実践で感覚をつかむだけね」
天々城
「お前、無駄に記憶力はいいからナ。
一回生で文系科目の点数が良かったの、やたら自慢してただろう？」
クアトロドルフ
「アレはただの報告さ。
ボクはあくまで合同算術しかわからない」
さトぅー
「はいはい、もう論理を哲学って言わないでよね」
クアトロドルフ
「キミの話でなんとなくわかったから言わないよ、約束しよう」
さトぅー
「下手に約束なんてしないほうがいいわよ」
天々城
「クアトロドルフが復帰したところで、続きを話そう。
自然数には大きいとか小さいとかあるよナ」
エーリル
「100000000とかすごく大きい感じ」
ディアナ
「自然数では0が一番小さいですね」
天々城
「ペアノ算術では大小を定義できる。
これを使えば2つの数を比べて、大きい小さいがわかるってわけだ」
■≦の定義
m,n:項
l:変数記号
(m≦n) :⇔ (∃l ((m+l) = n))
天々城
「mとnにズレがあるってことだナ」
エーリル
「あー、そういう定義でいいのか」
天々城
「≦は⇒とよく似ている」
■thm2.15(≦の反射性)
n:変数記号
PA |- (∀n (n≦n))
proof
1 (n = n) [=の反射性]
2 (∀n ((n+0) = n)) [PA2]
3 ((n+0) = n) [∀el 2]
c:変数記号
4 (∃c ((n+c) = n)) [∃in 3]
5 (n≦n) [def≦ in 4]
■
ディアナ
「nはn以上ですかね。
ちょっと不思議な感じですけど」
天々城
「必ずズレがあるような大小関係も定義できるが、後回しだ。
次へ進む」
■thm2.16(≦の推移性)
m,n,l:変数記号
PA |- (∀m (∀n (∀l (((m≦n)∧(n≦l))⇒(m≦l)))))
proof
1 ((m≦n)∧(n≦l)) [ax]
c,d,e:変数記号
2 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [+の結合性]
3 (((m+c)+d) = (m+(c+d))) [AAel 2]
4 ((m+(c+d)) = ((m+c)+d)) [=の可換性 3]
5 (m≦n) [∧elR 1]
6 (∃c ((m+c) = n)) [def≦ el 5]
7 ((m+c) = n) [ax]
8 (((m+c)+d) = (n+d)) [項の代入原理 7]
9 (n≦l) [∧elL 1]
10 (∃d ((n+d) = l)) [def≦ el 9]
11 ((n+d) = l) [ax]
12 ((m+(c+d)) = l) [=の3推移性 4,8,11]
13 (∃e ((m+e) = l)) [∃in 12]
14 (m≦l) [def≦ in 13]
15 (((n+d) = l)⇒(m≦l)) [⇒in 14 el 11]
16 (∀d (((n+d) = l)⇒(m≦l))) [∀in 15]
17 (m≦l) [∃el 10,16]
18 (((m+c) = n)⇒(m≦l)) [⇒in 17 el 7]
19 (∀c (((m+c) = n)⇒(m≦l))) [∀in 18]
20 (m≦l) [∃el 6,19]
21 (((m≦n)∧(n≦l))⇒(m≦l)) [⇒in 20 el 1]
22 (∀l (((m≦n)∧(n≦l))⇒(m≦l))) [∀in 21]
23 (∀n (∀l (((m≦n)∧(n≦l))⇒(m≦l)))) [∀in 22]
24 (∀m (∀n (∀l (((m≦n)∧(n≦l))⇒(m≦l))))) [∀in 23]
■
エーリル
「今までの証明となんか雰囲気が違う」
天々城
「∃が出てくるからナ。
大体長くなるのは仕方ない」
エーリル
「∃こわい」
天々城
「次に≦の『反対称性』っていうのを証明する」
クアトロドルフ
「……これちょっとヘンだね。
反対称性を証明しようとすると妙に引っかかる」
天々城
「暗算したのか？」
クアトロドルフ
「いや、感だよ」
天々城
「そうか。いやまあ、これが実際引っかかるんだ。
だから先に引っかかりを倒しておくぞ」
■thm2.17
0:定数記号
c,d:変数記号
+:項数2の関数記号
PA |- (∀c (∀d (((c+d) = 0)⇒(c = 0))))
proof
1 (∀n ((n+0) = n)) [PA2]
2 ((c+0) = c) [∀el 1]
3 (c = (c+0)) [=の可換性 2]
4 ((c+0) = 0) [ax]
5 (c = 0) [=の推移性 3,4]
6 (((c+0) = 0)⇒(c = 0)) [⇒in 5 el 4]
k:変数記号
7 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
8 ((c+S(k)) = S((c+k))) [AAel 7]
9 (S((c+k)) = (c+S(k))) [=の可換性 8]
10 ((c+S(k)) = 0) [ax]
11 (S((c+k)) = 0) [=の推移性 9,10]
12 (∀n (￢(S(n) = 0))) [PA1]
13 (￢(S((c+k)) = 0)) [∀el 12]
14 (c = 0) [explosion 12,13]
15 (((c+S(k)) = 0)⇒(c = 0)) [⇒in 14 el 10]
16 ((((c+k) = 0)⇒(c = 0)) ⇒ (((c+S(k)) = 0)⇒(c = 0))) [⇒in 15]
17 (∀k ((((c+k) = 0)⇒(c = 0)) ⇒ (((c+S(k)) = 0)⇒(c = 0)))) [∀in 16]
18 (∀d (((c+d) = 0)⇒(c = 0))) [数学的帰納法 6,17]
19 (∀c (∀d (((c+d) = 0)⇒(c = 0)))) [∀in 18]
■
天々城
「2つの自然数を足して0になったら必ず片方は0になる。
ちょっと計算すれば、当然両方とも0だナ」
エーリル
「PA1をはじめて使った」
ディアナ
「これを使うんですか？」
天々城
「そうだ」
■thm2.18(≦の反対称性)
m,n:変数記号
PA |- (∀m (∀n (((m≦n)∧(n≦m))⇒(m=n))))
proof
1 ((m≦n)∧(n≦m)) [ax]
c,d,l:変数記号
2 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [+の結合性]
3 (((m+c)+d) = (m+(c+d))) [AAel 2]
4 ((m+(c+d)) = ((m+c)+d)) [=の可換性 3]
5 (m≦n) [∧elR 1]
6 (∃c ((m+c) = n)) [def≦ el 5]
7 ((m+c) = n) [ax]
8 (((m+c)+d) = (n+d)) [項の代入原理 7]
9 (n≦m) [∧elL 1]
10 (∃d ((n+d) = m)) [def≦ el 9]
11 ((n+d) = m) [ax]
12 (∀n ((n+0) = n)) [PA2]
13 ((m+0) = m) [∀el 12]
14 (m = (m+0)) [=の可換性 13]
15 ((m+(c+d)) = (m+0)) [=の4推移性 4,8,11,14]
16 (∀m (∀n (∀l (((l+m) = (l+n))⇒(m = n))))) (+の左簡約律)
17 (((m+(c+d)) = (m+0))⇒((c+d) = 0)) [AAel 15]
18 (∀c (∀d (((c+d) = 0)⇒(c = 0)))) [thm2.17]
19 (((c+d) = 0)⇒(c = 0)) [AAel 18]
20 (((m+(c+d)) = (m+0))⇒(c = 0)) [⇒の推移性 17,19]
21 (c = 0) [⇒el 15,20]
22 ((m+c) = (m+0)) [項の代入原理 21]
23 ((m+0) = (m+c)) [=の可換性 22]
24 (m = n) [=の3推移性 14,23,7]
25 (((n+d) = m)⇒(m = n)) [⇒in 24 el 11]
26 (∀d (((n+d) = m)⇒(m = n))) [∀in 25]
27 (m = n) [∃el 10,26]
28 (((m+c) = n)⇒(m = n)) [⇒in 27 el 7]
29 (∀c (((m+c) = n)⇒(m = n))) [∀in 28]
30 (m = n) [∃el 6,29]
31 (((m≦n)∧(n≦m))⇒(m = n)) [⇒in 30 el 1]
32 (∀n (((m≦n)∧(n≦m))⇒(m = n))) [∀in 31]
33 (∀m (∀n (((m≦n)∧(n≦m))⇒(m = n)))) [∀in 32]
■
天々城
「証明は+の可換性くらいの難易度だろうナ」
ディアナ
「これは⇔inとよく似てますね」
天々城
「≦と=はきっと仲がいいんだろう」
エーリル
「反対称性の証明えぐい」
