我々は曖昧過ぎた

IsabelleやCoqだけを責めることは出来ないな。

論理学の用語や概念が曖昧だったんだよな。ものごとをハッキリさせるはずの学問が曖昧な記述で済ませていた。だから、ソフトウェア実装でも曖昧な概念と用語法が引き継がれ、混乱がより悪化した、という事情だろう。

例えば、「証明図」にしても、正しい証明図、たんなる図形、定理の証明図、派生規則（derived rule）の図、証明図のシェマなどは違う。推論図のシェマにしろ、シェマ変数の型（構文範疇）で解釈が変わる。こういう差異を明確にしないで、イイカゲンにやってきたわけだ。

ほんとにダメだなー。