ヒルベルト流と自然演繹
〇健全な研究室
エーリル
「そろそろこの世界に体を固定するための魔力が切れそう」
天々城
「魔力が切れたらどうなるんだ?」
エーリル
「元の世界に戻ることになる」
さトぅー
「私、エーリルさんがエルフっていうのまだ信じてないからね」
エーリル
「エルフなんですけど……」
天々城
「エルフでも人間でもどっちでもいい。
すべては数学が強力な言語ということに集約される」
エーリル
「強力な言語。強い」
さトぅー
「はいはい、じゃあ続きね。
Ax1,Ax2,Ax3,⇒elの4つからG0をはじめたじゃない?」
エーリル
「うん」
さトぅー
「この論理体系はヒルベルト流って呼ばれてて、推論規則をできるだけ少なくしてるの」
エーリル
「最終奥義使いそう」
天々城
「────ヒルベルト流、最終奥義ッ!」
エーリル
「強そう」
さトぅー
「今から、⇒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のみでできたこの言語を自然演繹"という。
そして、さっきの証明で次のことがわかった」
『ヒルベルト流と自然演繹は同じ能力をもった言語』
エーリル
「同じ能力をもった言語。そういうのもあるのか」
さトぅー
「やってみて感じてるはずだけど、この二つの言語は長所と短所がある」
天々城
「俺がまとめよう」
ヒルベルト流:
長所:メタ定理の証明が簡単
短所:証明に出てくる論理式がクソ長くて爆発する
自然演繹:
長所:自然言語っぽくてわかりやすい、
証明も証明に出てくる論理式もそんなに長くない
短所:演繹定理がわかってないと文法ミスで爆発する、
メタ定理の証明で推論規則ごと場合分けしないといけないときは場合分けが多すぎて爆発する
エーリル
「爆発する……つまり爆発則ッ!」
さトぅー
「爆発はしないと思う。
自然演繹から話をはじめなかったのは、公理を消すときのミスがあるから」
天々城
「文法ミスはそもそもダメだからナ。
演繹定理わかってたら公理を消したあと、言語そのものが切り替わってそれまでの証明に使えない論理式が出てくると気づくはずだ」
エーリル
「爆発則ッ!」ピカッ
さトぅー
「なんか光ってない?」
エーリル
「ごめん、やっぱり無理みたい。
こっちの世界に長くとどまりすぎた」輝きが増す
さトぅー
「ほんとになんかヤバそうなんだけど」
天々城
「さトぅーさんが爆発はしないとかフラグ建てるからだよ……」
さトぅー
「爆発するって言い出したの天々城じゃない!」
天々城
「あ、そうだ。練習用にG0の定理を書いたメモをあげよう。
これであっちでもG0が堪能できるナ」
エーリル
「ありがとう、ありがとう……」
\カッ/
さトぅー
「消えた。……本当にエルフだったのね」
天々城
「信じてなかったのかよ。
アレはどうみても賢者エルフ」
さトぅー
「それとねえ……」
天々城
「なんだ?」
さトぅー
「爆発するとか言って人のせいにするのはどうかと思うの」指関節を極める
天々城
「あっ、あっ」グギギギ