それが矛盾したらヤバイ
〇健全な研究室
研究室にやってきた賢者エルフの疑問に、天々城は堂々と答えた。
天々城
「ド・モルガンは黒魔法だ」
エーリル
「やっぱり！？ そうだと思ったのよね！」
さトぅー
「嘘はダメ」
エーリル
「嘘！？ そんなぁ……」
さトぅー
「定理に発見者や貢献した人の名前がつくことがあるの。
ド・モルガンの法則は、200年くらい前の数学者オーガスタス・ド・モルガンにちなんだものらしい」
天々城
「へー、数学史はよく知らないからフルネームははじめて聞いたナ」
エーリル
「なら、私が定理を見つけたら『エーリルの法則』とか名前つくのよね？」
天々城
「その理論だと、賢者エルフの地元の言葉は『エーリル語』になるぞ」
エーリル
「言われてみるとなんかこう、恥ずかしい」
天々城
「だろ？ 俺はこういうの苦手なんだよナ」
さトぅー
「意外ね。結構好きそうなイメージなんだけど」
天々城
「太極圏とかパンルヴェ方程参式なら許す」
さトぅー
「私は許さない」
*******************
さトぅー
「それで、質問って？」
エーリル
「∧、∨、⇔って可換性があるから、⇒はどうなんだろうって思ったの」
さトぅー
「⇒に可換性はないわね、結合性もない」
エーリル
「なんで？」
さトぅー
「意味を考えたら当たり前……ってダメか」
天々城
「意味論はやってないからナ。
ただこんなことはできる」
■meta thm1.0
すべての論理式φ,ψについて{(φ⇒ψ)} |- (ψ⇒φ)
ならば
{}|-⊥
proof
1 (ρ⇒ρ) [⇒の反射性]
2 (⊥⇒(ρ⇒ρ)) [⇒in 1]
3 ((ρ⇒ρ)⇒⊥) [すべての論理式φ,ψについて{(φ⇒ψ)} |- (ψ⇒φ)]
4 ⊥ [⇒el 1,3]
■
さトぅー
「なるほど、確かにそこまでなら意味論を使わないで証明できるわね」
エーリル
「え、公理なしで矛盾したらどんな論理式も証明できてマズイんじゃ……」
天々城
「その『マズイ』の部分が証明できれば決着だ。
ヒントを言っておこう」
■meta thm1.1
{} |- ⊥ではない。
■
天々城
「つまり公理系{}は矛盾しないが、すべての論理式φ,ψについて{(φ⇒ψ)} |- (ψ⇒φ)ならば{}|-⊥だからメタな矛盾をしてしまう。
だから、メタな￢inを使えば、{(φ⇒ψ)} |- (ψ⇒φ)ではない論理式φ,ψが存在するとわかるわけだ」
エーリル
「待って待って。メタな矛盾とメタな￢inはなんとなくわかるけど、なんで{(φ⇒ψ)} |- (ψ⇒φ)ではない論理式φ,ψが存在するってわかったの？」
天々城
「──なあ、さトぅーさん」
さトぅー
「言いたいことはわかるわよ、論理学の初歩は最低限やってるつもりだから。
で、私がやるの？」
天々城
「そうだよ」
さトぅー
「はいはいわかった。
代わりになにか甘いもの買ってきて。それで許してあげる」
天々城
「任せろ。トーラスを1ダース買ってきてやる」
エーリル
「あの、なにがはじまるんです？」
天々城
「一階述語論理だ」
