全順序律
〇健全な研究室
天々城
「自然数は小さい数から大きくなるように、『一直線』に並べられる。
まあ、nとS(n)の間に自然数は無いからスカスカだがナ」
エーリル
「言われてみればそうかも」
ディアナ
「『一直線』じゃないようなモノがあるんですか？」
天々城
「自然数じゃない相手なら、木みたいに枝分かれするモノがある。
こういうケースは反射性、推移性、反対称性まではうまく証明できたとしても、別の枝にあるモノの大小がわからない」
ディアナ
「同じ枝にないと、比べられないということでしょうか」
天々城
「そうだナ。比較不能とかいうが、どんな2つの自然数も比較不能にならない。
つまり、自然数m,nについてm≦nまたはn≦mが証明できて、自然数を並べた木はまっすぐ枝分かれせずに伸びていく。
クアトロドルフ、証明は思いつくか？」
クアトロドルフ
「ボクかい？ そうだね……。
多分、今までの中で一番難しいと思うよ。
隣の数が思ったより遠いのが定理に影響してるんだと思うけど、証明はわからないね」
天々城
「確かに、今までの中なら難しい方だろう。
当然、倒すには武器を揃えるしかない」
エーリル
「武器を揃える」
■thm2.19(≦の最小元)
0:定数記号
m:変数記号
PA |- (∀m (0≦m))
proof
1 (∀n ((0+n) = n)) [+の左単位元]
2 ((0+m) = m) [∀el 1]
3 (∃l ((0+l) = m)) [∃in 2]
4 (0≦m) [def≦ 3]
5 (∀m (0≦m)) [∀in 4]
■
天々城
「これはディアナ姫が言っていた気がする」
ディアナ
「ええ。この証明では単位元がうまく効いてるんですね」
天々城
「0は自然数の始まりをやってるからナ。
+では単位元、×では吸収元、≦では最小元。
それぞれでいい仕事をしてくれる」
■thm2.20
k:変数記号
S:項数1の関数記号
+:項数2の関数記号
PA |- (∀k ((k+1) = S(k)))
proof
1 1 = S(0) [1の定義]
2 ((k+1) = (k+S(0))) [項の代入原理 1]
3 (∀m (∀n ((m+S(n)) = S((m+n))))) [PA3]
4 ((k+S(0)) = S((k+0))) [AAel 3]
5 (∀n ((n+0) = n)) [PA2]
6 ((k+0) = k) [∀el 5]
7 (S((k+0)) = S(k)) [項の代入原理 6]
8 ((k+1) = S(k)) [=の３推移性 2,4,7]
9 (∀k ((k+1) = S(k))) [∀in 8]
■
天々城
「こっちは賢者エルフが言っていたナ」
エーリル
「ほら、私の言った通りでしょ？」
天々城
「Sと+1が実質同じとわかった。
コイツから新しい武器を作る」
■thm2.21
k:変数記号
S:項数1の関数記号
PA |- (∀k (k≦S(k)))
proof
1 (∀k ((k+1) = S(k))) [thm2.20]
2 ((k+1) = S(k)) [∀el 1]
3 (∃l ((k+l) = S(k))) [∃in 2]
4 (k≦S(k)) [def≦ in 3]
5 (∀k (k≦S(k))) [∀in 4]
■
エーリル
「次の方が大きいのは当たり前だった」
クアトロドルフ
「鬼門はまだ証明してないね」
天々城
「今から証明する。
例えば、(1≦2)なら((1+1)≦2)って感じに、うまく条件が揃えば+1したところで順序は変わらない。
これが証明の鬼門になるんだが、証明本体よりこっちの方が難しい」
■thm2.22
k.m:変数記号
S:項数1の関係記号
PA |- (∀k (∀m (((k≦m)∧(￢(k = m)))⇒(S(k)≦m))))
proof
a,n:変数記号
1 ((k≦m)∧(￢(k = m))) [ax]
2 (k≦m) [∧elR 1]
3 (∃a ((k+a) = m)) [def≦ el 2]
4 ((k+a) = m) [ax]
5 (￢(k = m)) [∧elL 1]
6 (∀m ((m = 0)∨(∃n (m = S(n))))) [thm2.1]
7 ((a = 0)∨(∃n (a = S(n)))) [∀el 6]
8 (a = 0) [ax]
9 ((k+a) = (k+0)) [項の代入原理 8]
10 ((k+0) = (k+a)) [=の可換性 9]
11 (∀n ((n+0) = n)) [PA2]
12 ((k+0) = k) [∀el 11]
13 (k = (k+0)) [=の可換性 12]
14 (k = m) [=の推移性 13,10,4]
15 (S(k)≦m) [explosion 14,5]
16 ((a = 0)⇒(S(k)≦m)) [⇒in 15 el 8]
17 (∃n (a = S(n))) [ax]
18 (a = S(n)) [ax]
19 ((k+a) = (k+S(n))) [項の代入原理 18]
20 ((k+S(n)) = (k+a)) [=の可換性 19]
21 (∀k (∀m ((k+S(m)) = (S(k)+m)))) [thm2.4]
22 ((k+S(n)) = (S(k)+n)) [AAel 21]
23 ((S(k)+n) = (k+S(n))) [=の可換性 22]
24 ((S(k)+n) = m) [=の推移性 23,20,4]
25 (∃n ((S(k)+n) = m)) [∃in 24]
26 (S(k)≦m) [def≦ in 25]
27 ((a = S(n))⇒(S(k)≦m)) [⇒in 26 el 18]
28 (∀n ((a = S(n))⇒(S(k)≦m))) [∀in 27]
29 (S(k)≦m) [∃el 17,28]
30 ((∃n (a = S(n)))⇒(S(k)≦m)) [⇒in 29 el 17]
31 (S(k)≦m) [∨el 7,16,30]
32 (((k+a) = m)⇒(S(k)≦m)) [⇒in 31 el 4]
33 (∀a (((k+a) = m)⇒(S(k)≦m))) [∀in 32]
34 (S(k)≦m) [∃el 3,33]
35 (((k≦m)∧(￢(k = m)))⇒(S(k)≦m)) [⇒in 34 el 1]
36 (∀m (((k≦m)∧(￢(k = m)))⇒(S(k)≦m))) [∀in 35]
37 (∀k (∀m (((k≦m)∧(￢(k = m)))⇒(S(k)≦m)))) [∀in 36]
■
エーリル
「数学的帰納法なしで37行……」
天々城
「短くなるように努力したんだがナ。
さトぅーさん、これより短い証明は知ってるか？」
さトぅー
「さあ、わからないわね。
実数も難しいけど、私にしてみれば自然数の時点で十分難しいから」
クアトロドルフ
「ボクは証明に強くないからわからないよ」
天々城
「それは知ってる」
エーリル
「武器は揃った？」
天々城
「ああ、無論だ」
■thm2.23(≦の全順序律)
m,n:変数記号
PA |- (∀m (∀n ((m≦n)∨(n≦m))))
1 (∀m (0≦m)) [≦の最小元]
2 (0≦m) [∀el 1]
3 ((m≦0)∨(0≦m)) [∨in 2]
k,l:変数記号
4 (∀k (k≦S(k))) [thm2.21]
5 (k≦S(k)) [∀el 4]
6 ((m≦k)∨(k≦m)) [ax]
7 (m≦k) [ax]
8 ((m≦k)∧(k≦S(k))) [∧in 7,5]
9 (∀m (∀n (∀l (((m≦n)∧(n≦l))⇒(m≦l))))) [≦の推移性]
10 (((m≦k)∧(k≦S(k))⇒(m≦S(k))) [AAel 9]
11 (m≦S(k)) [⇒el 8,10]
12 ((m≦S(k))∨(S(k)≦m)) [∨inR 11]
13 ((m≦k)⇒((m≦S(k))∨(S(k)≦m))) [⇒in 12 el 7]
14 (k≦m) [ax]
15 (((k = m))∨(￢(k = m))) [排中律]
16 (k = m) [ax]
17 ((k≦S(k))⇔(m≦S(k))) [論理式の代入原理 16]
18 (m≦S(k)) [⇔elL 5,17]
19 ((m≦S(k))∨(S(k)≦m)) [∨inR 18]
20 ((k = m)⇒((m≦S(k))∨(S(k)≦m))) [⇒in 19 el 16]
21 (￢(k = m)) [ax]
22 ((k≦m)∧(￢(k = m))) [∧in 14,21]
23 (∀k (∀m (((k≦m)∧(￢(k = m)))⇒(S(k)≦m)))) [thm2.22]
24 (((k≦m)∧(￢(k = m)))⇒(S(k)≦m)) [AAel 23]
25 (S(k)≦m) [⇒el 22,24]
26 ((m≦S(k))∨(S(k)≦m)) [∨inL 25]
27 ((￢(k = m))⇒((m≦S(k))∨(S(k)≦m))) [⇒in 26 el 21]
28 ((m≦S(k))∨(S(k)≦m)) [∨el 15,20,27]
29 ((k≦m)⇒((m≦S(k))∨(S(k)≦m))) [⇒in 28 el 14]
30 ((m≦S(k))∨(S(k)≦m)) [∨el 6,13,29]
31 (((m≦k)∨(k≦m))⇒((m≦S(k))∨(S(k)≦m))) [⇒in 30 el 6]
32 (∀k (((m≦k)∨(k≦m))⇒((m≦S(k))∨(S(k)≦m)))) [∀in 31]
33 (∀n (((m≦n)∨(n≦m)) [数学的帰納法 3,32]
34 (∀m (∀n (((m≦n)∨(n≦m))) [∀in 33]
■
天々城
「この証明は、kが数学的帰納法で進んでいくときにmを超える前、一致、超えた後で場合分けをしている。
はじめから自然数が一直線に並べられるってことを知ってるような証明だナ」
ディアナ
「こういう証明ができるとわかるのは才能なんでしょうかね」
天々城
「なんとも言えないナ。
経験的にわかることもあるし、試行錯誤でわかることもある。
百年に一人くらいお前は未来から来たんじゃないかってヤツもいる」
クアトロドルフ
「ほら、ボクの言った通りになっただろう？」
さトぅー
「ぼんやりした言い方でよくわからなかったわ」
クアトロドルフ
「その言い方は傷つくよ？」
天々城
「感覚派と論理派が一緒にいるのはマズいんだよなあ……」
