含意、随伴、両側シーケント、片側シーケント

例の話の続き。

両側シーケント計算を片側シーケント計算に還元できる場合がある。片側には右側と左側がある。この状況を分析してみると、モノイド圏の閉性（closedness, closure）が背後にある。そして閉性は、随伴により記述できる。

以下、モノイド積に対称性やブレイディングを一切仮定しない。古典論理なども扱えるように（いや、扱えないけどさ^^;）、モノイド積が∧、∨の2つあるとする。単に2つのモノイド積があるだけでは何にも面白くないのだが、2つのモノイド積の関連性とか一貫性はひとまず置いておく。∧の単位対象がT、∨の単位対象が⊥とする。

圏Cが上で述べた∧、∨、T、⊥を持つとして、典型的含意は4種類考えられる。それぞれ、o--, --o, x--, --x で表す。

1. C(A∧B, C) ＝ C(A, C o-- B)
2. C(A∧B, C) ＝ C(B, A --o C)
3. C(A, B∨C) ＝ C(B --x A, C)
4. C(A, B∨C) ＝ C(A x-- C, B)

o-- と --o は非対称なコンパクト論理の段階で既に考えていたもの。--x と x-- は今まで出てない。随伴で考えると：

1. (-∧B) -| (- o-- B)
2. (A∧-) -| (A --o -)
3. (B --x -) -| (B∨-)
4. (- x-- C) -| (-∨C)

ハイフンがいっぱい出てくるが、無名変数、随伴記号（逆ターンスタイル）の一部、含意記号の一部なのでヨロシク。

さて、両側シーケントを右片側シーケントに変換する原理は次。

  A → B

 -------------

  T∧A → B

 -------------

  T → B o-- A

  A → B

 -------------

  A∧T → B

 -------------

  T → A --o B

これは演繹定理だ。それに対して、両側シーケントを左片側シーケントに変換するときは：

  A → B

 -------------

  A → B∨⊥

 -------------

  B --x A → ⊥

  A → B

 -------------

  A → ⊥∨B

 -------------

  A x-- B → ⊥

古典論理やスターを持つコンパクト論理なら、B --x A は ¬B∧A として与えられるから、A |- B ⇔ ¬B, A |- ⊥ という分解原理のような形となる。

演繹定理や分解原理（だったか？Prologとかの原理）は、古典論理では成立するが、どんな論理でも成立するとは限らない。対称性が乏しい圏では、右片側シーケント化と左片側シーケント化が全然異なる状況になる可能性がある（どっちかはできないとか）。

ある圏のシーケント計算が右片側にできたとする。すると、Δ⇒Γ が証明できることと、⇒R(Δ;Γ) が証明できることが同値になる。ここで、R(Δ; Γ) は、Δを右に寄せた結果である。このRは、任意の射を、Tからの射に変換する働きを持つ。つまり、A, Bに対して対象 R_A,Bを割り当て、f:A→B に対して、ρ_A,B(f):T→R_A,Bを対応させるオペレータになる。オペレータを推論図で書くなら：

    A → B

 ------------[ρ(A,B)]

  T → R(A,B)

圏Cが閉じている、つまり指数（べき）を持つなら、オペレータ(R_{A, B}, ρ_{A, B})を指数を用いて具体的に表示できることになる。実際、Rは指数演算そのものだし、ρはフルカリー化によって与えられる。

ハロ多圏構成のテクニックを使うと、モノイド圏なら何に対してもシーケント計算が定義できる。閉じた圏なら片側シーケント計算も構成できる。片側シーケント計算は自然演繹と似たようなものなので、ある条件下では圏の自然演繹計算も構成できることになる。やっぱりハロ多圏構成は便利だ。

インフォーマルな道具として便利なのはわかったが、ハロ多圏の形式的な定義は出来てないから、考えないとな。