シーケント計算の再解釈 1

シーケント計算をリーズニング構成の計算と考える。できるだけ少ないリーズニングで計算をしたい。

リーズニングを少なくするには、プリミティブな導出を揃える。

∧-モノイド構造	∨-モノイド構造
![A]	Θ[A]
Δ[A]	∇[A]
π1[A, B]	ι1[A, B]
π2[A, B]	ι2[A, B]
X[A, B]	X[A, B]
A∧￢A → ⊥	T → A∨￢A

カット以外の構造規則はすべて、PreComp, PostComp で実現できる。

1. A-増 左： PreComp[![A]]
2. A-増 右： PostComp[Θ[A]]
3. A-減 左： PreComp[Δ[A]]
4. A-減 右： PostComp[∇[A]]
5. (A, B)-換 左： PreComp[X[A, B]]
6. (A, B)-換 右： PostComp[X[A, B]]

論理規則：

1. ∧ 左1 ： PreComp[π1[A, B]]
2. ∧ 左2 ： PreComp[π2[A, B]]
3. ∨ 左1 ： PostComp[ι1[A, B]]
4. ∨ 左2 ： PostComp[ι2[A, B]]

残るのは、

1. ∧ 右、∀ 右
2. ∨ 左、∃ 左
3. → 左