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

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

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

エラーが発生しました。

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

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

ペアノ算術

〇健全な研究室



クアトロドルフ

「なにが起こっているのかわからないんだけど、誰か説明してくれるかな?」


天々城

「見えることがすべてだ。

 言葉にしないとわからないのか?」


クアトロドルフ

「小さな女の子と美女がコスプレをしてるって事実を受け入れろってことかい?」


ディアナ

「む……」


天々城

「わかったわかった。

 今はそういうことにしておいてやる」


クアトロドルフ

「それにしたって、こんな小さな女の子に鎧を着せるなんて正気か?

 お嬢ちゃん、無理に物騒なものを着なくてもいいんだよ」


ディアナ

「天々城さん、この者は一体」


天々城

「イケメンで()特待生のクアトロドルフ」


クアトロドルフ

「ドーナツをあげるから、中二病患者の言うことなんか聞かなくてもいいんだよ」


さトぅー

「それ私のドーナツ」(指関節炸裂


クアトロドルフ

「■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■!」(指が逆方向に曲がる


天々城

「さトぅーさん、やりすぎ」


さトぅー

「エーリルさん、ドーナツ食べる?」


エーリル

「食べるー」(魔力回復


ディアナ

「……」


さトぅー

「ディアナ姫もどうぞ」


ディアナ

「お言葉に甘えて……甘っ!」


天々城

「買ったの俺なんだけどナ」


クアトロドルフ

「あぁあ、あぁあああ」


天々城

「お前、ホントになにしにきたんだ?」


ディアナ

「さトぅーさん……」


さトぅー

「急にどうしt……あァッ!」


ディアナ

「エーリルが残りを全部食べてしまって……」


エーリル

「魔力回復した」


さトぅー

「天々城!」


天々城

「俺はもう買わないからナ。

 しかも食べてないし」


さトぅー

「くッ……」


天々城

「お前らもう食っただろ。

 今日はなにするつもりだったんだ?」


さトぅー

「ペアノ算術」


天々城

「はー、なるほどナ。準備が整ったってわけだ。

 クアトロドルフ、お前は運がいいぞ」


クアトロドルフ

「どこが!? 天国が見えたんだよ!?」


天々城

「今から自然数をやるそうだ。

 しかもさトぅーさんに手を握ってもらったんだろ?」


クアトロドルフ

「アレは関節破壊だよ!」


天々城

「同情するレベルでその通りなんだよナあ……」


さトぅー

「あの、はじめてもいいかしら」


天々城、クアトロドルフ

「アッハイ」



ペアノ(Peano )(Arith)(metic)/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(数学(mathem)(atical)帰納( indu)(ction))

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は代入と違うのでは?」


天々城

「自然言語で書くときの流儀だろうナ。

 しかもメタ証明だし」


ディアナ

「わかりました」


天々城

「次からは本格的に自然数の世界に突入する」


エーリル

「強い表現力だ……」

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

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

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

↑ページトップへ