もしも代入をミスったら
〇健全な研究室
エーリル
「そろそろ魔力切れそう」
天々城
「なら急がないとナ」
クアトロドルフ
「魔力？ なんの茶番だい？」
天々城
「中二病ごっこさ」
クアトロドルフ
「今の言い方、やけにリアリティがあったね。
キミの演技力は大したものだよ」
さトぅー
（実際、リアルなのよねえ……）
天々城
「最後に≦と+,×に関する定理を紹介しよう」
■thm2.24
m,n,l:変数記号
+:項数2の関数記号
PA |- (∀m (∀n (∀l ((m≦n)⇒((m+l)≦(n+l))))))
proof
c:変数記号
1 (m≦n) [ax]
2 (∃c ((m+c) = n)) [def≦ el 1]
3 ((m+c) = n) [ax]
4 (((m+c)+l) = (n+l)) [項の代入原理 3]
5 (∀m (∀n (∀l (((m+n)+l) = (m+(n+l)))))) [+の結合性]
6 (((m+c)+l) = (m+(c+l))) [AAel 5]
7 ((m+(c+l)) = ((m+c)+l)) [=の可換性 6]
8 (∀m (∀n ((m+n) = (n+m)))) [+の可換性]
9 ((l+c) = (c+l)) [AAel 8]
10 ((m+(l+c)) = (m+(c+l))) [項の代入原理 9]
11 (((m+l)+c) = (m+(l+c))) [AAel 5]
12 (((m+l)+c) = (n+l)) [=の４推移性 11,10,7,4]
13 (∃c (((m+l)+c) = (n+l))) [∃in 12]
14 ((m+l)≦(n+l)) [def≦ in 13]
15 (((m+c) = n)⇒((m+l)≦(n+l))) [⇒in 14 el 3]
16 (∀c (((m+c) = n)⇒((m+l)≦(n+l)))) [∀in]
17 ((m+l)≦(n+l)) [∃el 2,16]
18 ((m≦n)⇒((m+l)≦(n+l))) [⇒in 17 el 1]
19 (∀l ((m≦n)⇒((m+l)≦(n+l)))) [∀in 18]
20 (∀n (∀l ((m≦n)⇒((m+l)≦(n+l))))) [∀in 19]
21 (∀m (∀n (∀l ((m≦n)⇒((m+l)≦(n+l)))))) [∀in 20]
■
天々城
「これはmとnの順序がわかっているなら、lだけズラしても順序は変わらないって感じだな」
クアトロドルフ
「≦の全順序律に比べたら道なりに証明するだけだね。
比較的易しい証明じゃないかな」
ディアナ
「+を×に変えるとどうなるんですか？」
天々城
「×に変えても同様だ」
■thm2.25
m,n,l:変数記号
×:項数2の関数記号
PA |- (∀m (∀n (∀l ((m≦n)⇒((m×l)≦(n×l))))))
proof
c:変数記号
1 (m≦n) [ax]
2 (∃c ((m+c) = n)) [def≦ el 1]
3 ((m+c) = n) [ax]
4 (((m+c)×l) = (n×l)) [項の代入原理 3]
5 (∀m (∀n (∀l (((m+n)×l) = ((m×l)+(n×l)))))) [+×の右分配法則]
6 (((m+c)×l) = ((m×l)+(c×l))) [AAel 5]
7 (((m×l)+(c×l)) = ((m+c)×l)) [=の可換性 6]
8 (((m×l)+(c×l)) = (n×l)) [=の推移性 7,4]
9 (∃c (((m×l)+c) = (n×l))) [∃in 8]
10 ((m×l)≦(n×l)) [def≦ in 9]
11 (((m+c) = n)⇒((m×l)≦(n×l))) [⇒in 10 el 3]
12 (∀c (((m+c) = n)⇒((m×l)≦(n×l)))) [∀in 11]
13 ((m×l)≦(n×l)) [∃el 12]
14 ((m≦n)⇒((m×l)≦(n×l))) [⇒in 13 el 1]
15 (∀l ((m≦n)⇒((m×l)≦(n×l)))) [∀in 14]
16 (∀n (∀l ((m≦n)⇒((m×l)≦(n×l))))) [∀in 15]
17 (∀m (∀n (∀l ((m≦n)⇒((m×l)≦(n×l)))))) [∀in 16]
■
天々城
「つまりmとnにlを一緒に掛けても順序は変わらない」
クアトロドルフ
「ああ、こっちの方が易しいね。
+は可換性を使った分、証明が若干伸びるようだ」
ディアナ
「×も一緒なんですね」
天々城
「自然数はナ。
他のモノだと構造上の違いがあるせいで、≦と×に制限がつく」
さトぅー
「整数に拡張するだけで証明できないわよね。
実数くらいまでなら≦と+は生きてるんだけど」
天々城
「あ、そうだ。この話をしておかないとナ」
エーリル
「急ぎで」(ちょっと光る
天々城
「任せろ。
代入の定義(10)で∀や∃に捕まった変数を別の変数に変えるのがあったよナ」
ディアナ
「確かにありましたね。
なんでこんな回りくどいことをしてるのかと思っていました」
天々城
「その前に伝説の定理を紹介する」
■thm2.26
0:定数記号
PA |- (￢(1 = 0))
proof
1 (1 = S(0)) [1の定義]
2 ((￢(1 = 0))⇔(￢(S(0) = 0))) [論理式の代入原理 1]
3 (∀n (￢(S(n) = 0))) [PA1]
4 (￢(S(0) = 0)) [∀el 3]
5 ((￢(1 = 0)) [⇔elR 2,4]
■
クアトロドルフ
「伝説の定理というか、伝説の自明じゃないか。
その辺の動物でもわかることをわざわざ証明しなくてもいいだろう」
天々城
「今から意図的に文法ミスをするんだ。
最後くらい形式的にやらせてくれ」
■例：代入を間違える
x,m,n:変数記号
1 (∀x (x = x)) [Ax]
2 (x = x) [∀el 1]
3 (∃n (x = n)) [∃in 2]
4 (∀m (∃n (m = n))) [∀in 3]
5 (∃n ((n+1) = n)) [∀el 4 無理矢理[(n+1)/m]と代入する]
6 ((n+1) = n) [ax]
7 (∀n ((n+0) = n)) [PA2]
8 ((n+0) = n) [∀el 7]
9 (n = (n+0)) [=の可換性 8]
10 ((n+1) = (n+0)) [=の推移性 6,9]
11 (∀m (∀n (∀l (((l+m) = (l+n))⇒(m = n))))) [+の左簡約律]
12 (((n+1) = (n+0))⇒(1 = 0)) [AAel 11]
13 (1 = 0) [⇒el 10,12]
14 (￢(0 = 1)) [thm2.26]
15 ⊥ [⊥in 13,14]
16 ((n = (n+1))⇒⊥) [⇒in 15 el 6]
17 (∀n ((n = (n+1))⇒⊥)) [∀in 16]
18 ⊥ [∃el 5,17]
よってPA |- ⊥
■
エーリル
「PAが壊れた。代入許さん」(ピカッ
天々城
「(∃n (m = n))[(n+1)/m]を(∃n ((n+1) = n))と計算したのが原因だ。
そもそもmは∃に捕まってない変数なのに、代入した項で∃に捕まるのがマズい」
ディアナ
「自由変数は代入した項でも自由でなければならないということですか」
天々城
「そんな感じだナ。
次に∀inだ。これは使うときに公理を確認しないといけないが、わざと無視する」
■例：∀inを間違える
1 (1 = n) [ax]
2 (∀n (1 = n)) [公理に自由変数nがあるのに無理矢理∀in 1]
3 (1 = 0) [∀el 2]
4 (￢(1 = 0)) [thm2.26]
5 (￢(1 = n)) [￢in 3,4 el 1]
6 (∀n (￢(1 = n))) [∀in 5]
7 (￢(1 = 1)) [∀el 6]
8 (1 = 1) [=の反射性]
9 ⊥ [⊥in 8,7]
よってPA |- ⊥
■
エーリル
「PAが壊れた。∀in許さん」(ピカッ
天々城
「全パターンで証明できたから『すべて』を付けていい。
公理に自由変数が残っているときは、あるパターンでしか証明できてないから『すべて』を付けると矛盾することがある」
ディアナ
「∀inは∧inと似てるんでしたよね。
確かに一つだけ導いて∧inはおかしい」
天々城
「大体そんな感じだナ」
クアトロドルフ
「天々城くん、ちょっといいかな」
天々城
「いいぞ、ちょうど終わったところだ」
クアトロドルフ
「エルフのコスプレの彼女、光ってないかい？」
エーリル
「魔力が臨海突破ッ！」(光
天々城
「お前は知らないと思うが、女の子は光るんだよ」
ディアナ
「では私たちはこれで。
本日はありがとうございました」
エーリル
「ありがとー」
＼カッ／
クアトロドルフ
「き、消えた……？
天々城くん、キミは一体どんなトリックを使ったんだい？」
天々城
「マジカル三角圏」
クアトロドルフ
「マ、マジカル……なんだって？」
さトぅー
「お腹すいたし、私は帰るわ。じゃあね」
天々城
「クアトロドルフ、戸締りは任せた」
#さトぅー、天々城が退室しました#
クアトロドルフ
「えっ、えっ？」
