証明、項、射

トレース付きモノイド圏Cに意味を持つような形式的体系の項を考えると、その項はシーケント計算の証明に対応する。証明図の木構造がちょうど項の木構造に対応する。よって、項の変形は証明図の変形になっている。

さらに、項の値（意味）は圏Cの射だから、証明図、項、射に対応が付く。開いた証明図、開いた項を考えると、それは多変項関手になる。

この対応により、カット消去定理、項の準正規化が対応していることがわかる。これは、結び目理論のアレクサンダーの定理の類似物だが、結び目ではさらにマルコフの定理がある。証明系と項計算におけるマルコフの定理の類似は何だろう？