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

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

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

エラーが発生しました。

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

ブックマーク機能を使うにはログインしてください。
エルフに数学を装備するだけ  作者: めいぜんおーえす
二章:ことばを作るよー
26/51

ヒルベルト流と自然演繹

〇健全な研究室


エーリル

「そろそろこの世界に体を固定するための魔力が切れそう」


天々城

「魔力が切れたらどうなるんだ?」


エーリル

「元の世界に戻ることになる」


さトぅー

「私、エーリルさんがエルフっていうのまだ信じてないからね」


エーリル

「エルフなんですけど……」


天々城

「エルフでも人間でもどっちでもいい。

 すべては数学が強力な言語ということに集約される」


エーリル

「強力な言語。強い」


さトぅー

「はいはい、じゃあ続きね。

 Ax1,Ax2,Ax3,⇒elの4つからG0をはじめたじゃない?」


エーリル

「うん」


さトぅー

「この論理体系はヒルベルト(Hilbert)(system)って呼ばれてて、推論規則をできるだけ少なくしてるの」


エーリル

「最終奥義使いそう」


天々城

「────ヒルベルト流、最終奥義ッ!」


エーリル

「強そう」


さトぅー

「今から、⇒el,⇒in,¬elだけを使ってAx1,Ax2,Ax3を証明する」


エーリル

「……はい?」





■Ax1

{} |- (φ⇒(ψ⇒φ))


proof

1 φ [ax]

2 (ψ⇒φ) [⇒in 1]

3 (φ⇒(ψ⇒φ)) [⇒in 2 el 1]




■Ax2

{} |- ((φ⇒(ψ⇒ρ))⇒((φ⇒ψ)⇒(φ⇒ρ)))


proof

1 (φ⇒(ψ⇒ρ)) [ax]

2 (φ⇒ψ) [ax]

3 φ [ax]

4 ψ [⇒el 3,2]

5 (ψ⇒ρ) [⇒el 3,1]

6 ρ [⇒el 4,5]

7 (φ⇒ρ) [⇒in 6 el 3]

8 ((φ⇒ψ)⇒(φ⇒ρ)) [⇒in 7 el 2]

9 ((φ⇒(ψ⇒ρ))⇒((φ⇒ψ)⇒(φ⇒ρ))) [⇒in 8 el 1]




さトぅー

「ここまでは背理法を使ってないよね」


エーリル

「つまり、Ax3のために背理法が構えていると」



■Ax3

{} |- (((¬ψ)⇒(¬φ))⇒(φ⇒ψ))


proof

1 (¬ψ) [ax]

2 ((¬ψ)⇒(¬φ)) [ax]

3 (¬φ) [⇒el 1,2]

4 φ [ax]

5 ψ [¬el 4,3 el 1]

6 (φ⇒ψ) [⇒in 5 el 4]

7 (((¬ψ)⇒(¬φ))⇒(φ⇒ψ)) [⇒in 6 el 2]



エーリル

「マジだった」


天々城

「うーん、やっぱ演繹定理と背理法は性能壊れてるよナ。壊れ定理確定ですわ」


さトぅー

「Ax1,Ax2,Ax3みたいな論理的公理を持たないで、3つの推論規則⇒el,⇒in,¬elのみでできたこの言語を自然(natural)(dedu)(ction)"という。

 そして、さっきの証明で次のことがわかった」




『ヒルベルト流と自然演繹は同じ能力をもった言語』




エーリル

「同じ能力をもった言語。そういうのもあるのか」


さトぅー

「やってみて感じてるはずだけど、この二つの言語は長所と短所がある」


天々城

「俺がまとめよう」




ヒルベルト流:

長所:メタ定理の証明が簡単

短所:証明に出てくる論理式がクソ長くて爆発する



自然演繹:

長所:自然言語っぽくてわかりやすい、

   証明も証明に出てくる論理式もそんなに長くない

短所:演繹定理がわかってないと文法ミスで爆発する、

   メタ定理の証明で推論規則ごと場合分けしないといけないときは場合分けが多すぎて爆発する




エーリル

「爆発する……つまり爆発則ッ!」


さトぅー

「爆発はしないと思う。

 自然演繹から話をはじめなかったのは、公理を消すときのミスがあるから」


天々城

「文法ミスはそもそもダメだからナ。

 演繹定理わかってたら公理を消したあと、言語そのものが切り替わってそれまでの証明に使えない論理式が出てくると気づくはずだ」


エーリル

「爆発則ッ!」ピカッ


さトぅー

「なんか光ってない?」


エーリル

「ごめん、やっぱり無理みたい。

 こっちの世界に長くとどまりすぎた」輝きが増す


さトぅー

「ほんとになんかヤバそうなんだけど」


天々城

「さトぅーさんが爆発はしないとかフラグ建てるからだよ……」


さトぅー

「爆発するって言い出したの天々城じゃない!」


天々城

「あ、そうだ。練習用にG0の定理を書いたメモをあげよう。

 これであっちでもG0が堪能できるナ」


エーリル

「ありがとう、ありがとう……」




\カッ/




さトぅー

「消えた。……本当にエルフだったのね」


天々城

「信じてなかったのかよ。

 アレはどうみても賢者エルフ」


さトぅー

「それとねえ……」


天々城

「なんだ?」


さトぅー

「爆発するとか言って人のせいにするのはどうかと思うの」指関節を極める


天々城

「あっ、あっ」グギギギ

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

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

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

↑ページトップへ