CMLLとMILL

「コンパクト乗法的線形論理」でCMLL（Compact Multiplicative Linear Logic）の推論規則を出したが、MILL（Multiplicative Intuitionistic Linear Logic）も記しておこう。CMLLは意外と古典論理（∧と¬）に近くて、MILLと感じが違う。

CMLLとMILLを比較する； 構造規則に換（exchange）とカットがあるのは同じ。ただし、

1. MILLでは換は左（仮定、前件）のみ。
2. カットの形もMILLでは制限される。

公理がA |- A と |- I である点も同じ。ただし、|- I は、Iの右導入規則と位置づけられる（まー、どうでもいいけど）。

 Γ |- A

 -----------[I水増し, I導入 左]

 I,Γ |- A
  (なし)

 --------[I導入 右]

  |- I

MILLの×と⊃に関する論理的な推論規則。

 Γ,A,B |- C

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

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

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

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

 ---------------------[⊃導入 左]

 Γ,Δ,A⊃B |- C
 Γ,A |- B

 ------------[⊃導入 右]

 Γ |- A⊃B

自然演繹風な別な流儀。

 Γ |- A   Δ |- I

 --------------------[I消去]

 Γ,Δ |- A
 Γ |- A  Δ |- B

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

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

 -------------------------[×消去]

 Γ,Δ |- C
 Γ,A |- B

 ---------------------[⊃導入]

 Γ |- A⊃B
 Γ |- A⊃B   Δ |- A

 ---------------------[⊃消去]

 Γ,Δ |- B

念のため、CMLLを再掲。

 Γ |- Δ

 -----------[I導入 左]

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

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

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

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

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

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

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

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

 Γ |- Δ,¬A

この話題に関しては、

• Samson Abramsky, Ross Duncan "A categorical quantum logic" →http://www.mathstat.dal.ca/~selinger/qpl2004/PDFS/02Abramsky-Duncan.pdf （ローカルにも落とした）