ペアノ算術
〇健全な研究室
クアトロドルフ
「なにが起こっているのかわからないんだけど、誰か説明してくれるかな？」
天々城
「見えることがすべてだ。
言葉にしないとわからないのか？」
クアトロドルフ
「小さな女の子と美女がコスプレをしてるって事実を受け入れろってことかい？」
ディアナ
「む……」
天々城
「わかったわかった。
今はそういうことにしておいてやる」
クアトロドルフ
「それにしたって、こんな小さな女の子に鎧を着せるなんて正気か？
お嬢ちゃん、無理に物騒なものを着なくてもいいんだよ」
ディアナ
「天々城さん、この者は一体」
天々城
「イケメンで元特待生のクアトロドルフ」
クアトロドルフ
「ドーナツをあげるから、中二病患者の言うことなんか聞かなくてもいいんだよ」
さトぅー
「それ私のドーナツ」(指関節炸裂
クアトロドルフ
「■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■！」(指が逆方向に曲がる
天々城
「さトぅーさん、やりすぎ」
さトぅー
「エーリルさん、ドーナツ食べる？」
エーリル
「食べるー」(魔力回復
ディアナ
「……」
さトぅー
「ディアナ姫もどうぞ」
ディアナ
「お言葉に甘えて……甘っ！」
天々城
「買ったの俺なんだけどナ」
クアトロドルフ
「あぁあ、あぁあああ」
天々城
「お前、ホントになにしにきたんだ？」
ディアナ
「さトぅーさん……」
さトぅー
「急にどうしt……あァッ！」
ディアナ
「エーリルが残りを全部食べてしまって……」
エーリル
「魔力回復した」
さトぅー
「天々城！」
天々城
「俺はもう買わないからナ。
しかも食べてないし」
さトぅー
「くッ……」
天々城
「お前らもう食っただろ。
今日はなにするつもりだったんだ？」
さトぅー
「ペアノ算術」
天々城
「はー、なるほどナ。準備が整ったってわけだ。
クアトロドルフ、お前は運がいいぞ」
クアトロドルフ
「どこが！？ 天国が見えたんだよ！？」
天々城
「今から自然数をやるそうだ。
しかもさトぅーさんに手を握ってもらったんだろ？」
クアトロドルフ
「アレは関節破壊だよ！」
天々城
「同情するレベルでその通りなんだよナあ……」
さトぅー
「あの、はじめてもいいかしら」
天々城、クアトロドルフ
「アッハイ」
■ペアノ算術/PA
0:定数記号
S:項数1の関数記号
+,×:項数2の関数記号
m,n:変数記号
φ:論理式
PA0 (∀m (∀n ((S(m) = S(n))⇒(m = n))))
PA1 (∀n (￢(S(n) = 0)))
PA2 (∀n ((n+0) = n))
PA3 (∀m (∀n ((m+S(n)) = S((m+n)))))
PA4 (∀n ((n×0) = 0))
PA5 (∀m (∀n ((m×S(n)) = ((m×n)+m))))
PA6 (∀x_0...(∀x_k (((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m]))))⇒(∀m φ)) )...)
(x_0,...,x_kはfv(φ)に含まれるmでないすべての変数記号)
クアトロドルフ
「なんだいこれは、言葉がほとんどないじゃないか」
さトぅー
「……はい？」
天々城
「クアトロドルフは一階述語論理をやったことはあるのか？」
クアトロドルフ
「あれは哲学だろう？」
さトぅー
「数学です」(指関節炸裂
クアトロドルフ
「■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■！」(指が逆方向に曲がる
天々城
「イケメンはさトぅーさんに任せて、俺たちは先に進むか」
エーリル
「PA6って数学的帰納法のこと？」
天々城
「流石賢者エルフ、よく気づいたナ」
エーリル
「ということはSは+1か」
天々城
「素晴らしい。ただそれは証明がいるけどナ」
■thm2.0(数学的帰納法)
0:定数記号
S:項数1の関数記号
m,n:変数記号
φ:論理式
PA∪{(φ[0/m]),(∀n ((φ[n/m])⇒(φ[S(n)/m])))} |- (∀m φ)
proof
x_0,...,x_kはfv(φ)に含まれるmでないすべての変数記号とする。
1 (∀x_0...(∀x_k (((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m]))))⇒(∀m φ)) )...) [PA6]
2 (∀x_1...(∀x_k (((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m]))))⇒(∀m φ)) )...) [∀el 1]
:
:
k+1 (∀x_k (((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m]))))⇒(∀m φ)) ) [∀el k]
k+2 (((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m]))))⇒(∀m φ)) [∀el k+2]
k+3 (φ[0/m]) [ax]
k+4 (∀n ((φ[n/m])⇒(φ[S(n)/m]))) [ax]
k+5 ((φ[0/m])∧(∀n ((φ[n/m])⇒(φ[S(n)/m])))) [∧in k+3,k+4]
k+6 (∀m φ) [⇒el k+5,k+2]
■
天々城
「これで数学的帰納法のスキルが開放された」
エーリル
「強い」
ディアナ
「2行目からk+2行目までは∀elを適用し続けたんでしょうか」
天々城
「そうだナ……って、ディアナ姫は読めるのか？」
ディアナ
「エーリルから教えていただきました」
天々城
「そっちの世界は逸材の宝庫かよ」
ディアナ
「いえ、他のドワーフは残念ながら」
天々城
「なんか申し訳ないことを聞いてしまった」
ディアナ
「こういうのは時間がかかりますから、お気になさらず」
天々城
「気を取り直して先に進むぞ。
毎回∀elを乱射するのは面倒くさいから、次の定理でショートカットする。
さトぅーさん、∀を一気に外すのなんか名前ある？」
さトぅー
「うーん。全称閉包は∀∀って書くことあるけど、あれは閉論理式だから違うのよね。
クアトロドルフくんは何か知ってる？」
クアトロドルフ
「痛たた……。『すべて』がそんなに出てきたことないよ」
天々城
「まあ、普通の数学の言い回しだとそうだろうナ。
とりあえず、AAelでいくぞ」
さトぅー
「大体なんの略かわかったわ」
■meta thm2.0(AAel)
m:自然数
x_0,...,x_m:変数記号
φ:論理式
とする。
すべての自然数mについて
{(∀x_0 ...(∀x_m φ)...)} |- φ
proof
数学的帰納法で証明する。
・m=0のとき
1 (∀x_0 φ) [ax]
2 φ [∀el 1]
よって、すべての論理式φについて{(∀x_0 φ)} |- φ。
・m=nのとき、すべての論理式φについて
{(∀x_0 ...(∀x_n φ)...)} |- φとすると、m=n+1のとき、
1 (∀x_0 ...(∀x_n (∀x_(n+1)φ))...) [ax]
2 (∀x_(n+1)φ) [すべての論理式φについて{(∀x_0 ...(∀x_n φ)...)} |- φ]
3 φ [∀el 2]
よって、すべての論理式φについて{(∀x_0 ...(∀x_n (∀x_(n+1)φ))...)} |- φ。
数学的帰納法より、すべての自然数mについて{(∀x_0 ...(∀x_m φ)...)} |- φ。
■
エーリル
「言われてみれば外側の∀は全部外せるのか」
ディアナ
「m=nは代入と違うのでは？」
天々城
「自然言語で書くときの流儀だろうナ。
しかもメタ証明だし」
ディアナ
「わかりました」
天々城
「次からは本格的に自然数の世界に突入する」
エーリル
「強い表現力だ……」
