コンパクト論理の計算、推論規則と公理

圏論的な観点からいうと、シーケント計算て、圏のスジのような部分だけを議論している -- 圏をプレ順序集合に潰してしまうからな。シーケント計算では、圏の性質をキチンと捉えることはできない。が、単純化するもんだから計算も簡単になるメリットはある。

さてそれで、推論規則。CPは Composition and Product の略。

   Γ → Δ,Π  Π,Φ → Ψ

 ---------------------------[CP1]

     Γ,Φ → Δ,Ψ

  Φ,Π → Ψ   Γ → Π,Δ

 ---------------------------[CP2]

    Φ,Γ → Ψ,Δ

このCP1、CP2は強力。絵で描けば、多圏の結合の一種。

次が公理。

1. [id] A → A
2. [lunit] I,A → A と A → I,A
3. [runit] A,I → A と A → A,I

これで、モノイド圏の計算ができる。idはトートロジー、lunit, runitは、Iに関する増減になっている。

対称性を入れるには：

• [symm] A,B → B,A

これは換（Exchange）

双対（随伴）は次のようになる。

1. [unit-neg] I → ¬I と ¬I → I
2. [ev] A,¬A → I
3. [coev] I → ¬A,A

それと、含意の定義

1. ¬A,B → A⊃B と A⊃B → ¬A,B
2. A,¬B → A⊂B と A⊂B → A,¬B

コンパクト閉圏にモデルを取れば、次は意味的に言える。

1. 二重否定
2. 対偶
3. 演繹定理（カリー化、反カリー化）