まだまだ改善の余地がある。コンパクト論理に限定するとして、 論理式＝生成対象の集合 F から作った自由コンパクト圏 原子証明＝生成射＝シーケントの集合 S から作った自由コンパクト圏 コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent r…