自然演繹の正規形定理とデカルト閉圏

自然演繹の正規形定理は、直和を持つデカルト閉圏の等式的な公理系から出てしまう。つまり、直和を持つデカルト閉圏を計算するシステムのなかに自然演繹は埋め込めて、正規形定理は埋め込み先では自明になってしまう。

自明になってしまうのだけど、そこまで行くには長い長い前フリが必要になる。