■

授業第十六回目は、「論理結合子の意味とは何か」の続きで、前回のベルナップによる「保存拡大性」に関するメタ定理の証明の際に使用した「証明図の付け替え」という技法にスポットライトを当てます。この技法により保存拡大性が証明可能なため、「論理体系の本質とは、この証明図の付け替え技法が可能なことである」という考えが生まれてきました。
今回は、この技法を発展させた「インバージョン原理」、さらに体系に含まれる結合子がそれを満たしていることを証明するために必要な「証明の正規化可能性」という二つの重要な概念を紹介します。このどちらも、ダメットやプラヴィッツと言った多くの哲学者や論理学者によって、論理体系の満たすべき重要な性質と見なされています。
なお、「最小命題論理の任意の証明は正規化可能である」というメタ定理は、次回以降に紹介します。