■

授業第十六回目は、「論理結合子の意味とは何か」の続きで「反転原理」を取り上げます。前回紹介したように、トンクは体系を自明化するという本質的な欠陥を持っていましたが、トンクの導入規則は∨、除去規則は∧と同じであり、それ自身としては問題がないはずです。つまり、トンクを最小命題論理に付加する際に保存拡大性が壊れたことは、トンクにおいて導入規則と除去規則が不釣り合いであることが原因である、と言えるはずです。なので、今回は、「両者の釣り合いとは何か」を考えます。「反転原理」は、その釣り合いを表現するものなのです。
具体的には、前回のベルナップによる「保存拡大性」に関するメタ定理の証明の際に使用した「証明図の付け替え」という技法にスポットライトを当てます。この技法により保存拡大性が証明可能なため、「論理体系の本質とは、この証明図の付け替え技法が可能なことである」という考えが生まれてきました。今回は、この技法を発展させた「反転原理」、さらに体系に含まれる結合子がそれを満たしていることを証明するために必要な「証明の正規化可能性」という二つの重要な概念を紹介します。このどちらも、ダメットやプラヴィッツと言った多くの哲学者や論理学者によって、論理体系の満たすべき重要な性質と見なされています。
なお、「最小命題論理の任意の証明は正規化可能である」というメタ定理は、次回以降に紹介します。