ΨにΦ、ΨにΦ

論理学演習13番、簡単だよ。と言ってid:kzkに奨めてみた。もうすぐ三週間になるのに解けないという。そんなはずはないと思っていた。するとF-さんも、たいへん、という。そんなはずは無いと思って、id:kzkとF-さんの前で解いてみた。

5分後：うわーたいへんだーこれめんどいー（ペンを投げるぴらぴら）。

我に返ったぴらぴらは、自然演繹を思いだし、
シークエント計算 → 自然演繹 → ヒルベルト流 → シークエント計算
と、ぐるぐるまわりの証明を書くことにした。するとうまくいった。

ぴらぴら教の演繹体系は、自然演繹と定める。

ヒルベルト流の演繹体系をいじっていると、シュレディンガー音頭を思い出す。
modus ponens (φ→ψとφからψを導く)には、どんな仕草をあてはめればいいんだろう。

眠られぬ夜のためのヒルベルト流：
http://au.metamath.org/mpegif/mmtheorems.html

　　伝説の書物Principia Mathematicaの命題たちも、しっかり登場している…！