- 定義1： 論理式の集合（生成系）
- 定義2： 演繹閉な論理式の集合（順序閉包）
- 定義3： 証明〈推論規則〉の集合（生成系）
- 定義4： リーズニング閉な証明〈推論規則〉の集合（リーズニング閉包＝圏）
- 定義5： 生成系を持つ圏
- 定義5'： 指標〈生成系〉を持つ圏
また、
- 定義6： 定理の集合
- 定義6'： 名前に対する証明の割当の集合
- 定義7： 証明記述言語の構文モナドのクライスリ射
- 定義8： クライスリ射のクライスリ拡張である関手
定義5'と定義8では、圏と関手の違いがあるので、統合は無理。セオリー圏とセオリー関手とでも呼び分けるしかない。
