対称モノイド圏のシーケント計算

白旗さんの論文をもとにする。Compact Multiplicative Linear Logicのシーケント計算から、否定（極性）を除くと次のようになる。

Σをアルファベット（基礎記号集合）として、式（formula）は次のように定義する。

1. Σの元
2. I（IはΣに入らない）
3. (式+式) （括弧は適宜省略）

A, Bなどは式だとして、式の列をΓ, Δなど。Γ⇒Δがシーケント。公理は：

1. a∈Σとして、a⇒a
2. ⇒I

構造的推論規則、式の量は変わらない。

  Γ,A,B,Δ⇒Φ

  --------------[換 左; exchange left]

  Γ,B,A,Δ⇒Φ
  Γ⇒Δ,A,B,Φ

  --------------[換 右; exchange right]

  Γ⇒Δ,B,A,Φ
  Γ⇒Δ  Φ⇒Ψ

  ----------------[混合; mix]

  Γ,Φ⇒Δ,Ψ

導入規則、式（部分式も含める）の量は変わらず論理記号（+, I）が増える。

  Γ,A,B,Δ⇒Φ

  --------------[+導入 左]

  Γ,A+B,Δ⇒Φ
  Γ⇒Δ,A,B,Φ

  --------------[+導入 右]

  Γ⇒Δ,A+B,Φ
  Γ⇒Δ

  ----------[I導入; unit weakening]

  I,Γ⇒Δ

カットは式が減る。

  Γ⇒Δ,A  A,Φ⇒Ψ

  ------------------[切断; cut]

  Γ,Φ⇒Δ,Ψ

対称モノイド圏とは次の関係がある。

シーケント計算	対称モノイド圏
+	対象のモノイド積
I	モノイド単位
公理	恒等射
換	対称ブレイディング
混合	射のモノイド積（と対称）
切断	（部分的な）結合

コンパクト閉圏では次が追加される。

• Aが式ならA*も式である。

  Γ⇒A,Δ

  ----------[*導入 左]

  A*,Γ⇒Δ
  Γ,A⇒Δ

  ----------[*導入 右]

  Γ⇒Δ,A*