コンパクト乗法的線形論理

白旗さんのアレ（例えば、http://www.fbc.keio.ac.jp/~sirahata/Research/cmll.pdf）から推論規則を抜き出しておこう。

公理は、コンパクト閉圏C（モデルの圏）から適当に選んだ射達、ただしidは全部入れる。それと、|- I（Iは単位）。CがΣから生成されているなら、idとIとΣ（固有な公理に相当）を入れるといいだろう。

 Γ,A,B,Δ |- Σ

 ----------------[×導入 左]

 Γ,A×B,Δ |- Σ

 Γ |- Δ,A,B,Σ

 ----------------[×導入 右]

 Γ |- Δ,A×B,Σ
 Γ |- A,Δ

 ------------[¬導入 左]

 Γ,¬A |- Δ
 Γ,A |- Δ

 ------------[¬導入 右]

 Γ |- Δ,¬A

構造規則は、左右の換（exchange）、混合（mix）、カット。カットは、 Γ |- A,Δ と Σ,A |- Π からAをシングルカットする。Iに関してだけ右水増しができる。

 Γ |- Δ

 -----------[I水増し]

 I,Γ |- Δ

以上がCMLLのシーケント計算体系。結論がイッパイあるので、多圏で考えたほうがいいだろう。この計算は、自然演繹に対応する証明グラフとは相性がいいだろうが、ラムダ計算とはどうも相性が悪そうだ。右側を単一命題にすればいいのだが、対称性は崩れるな。