古典的片側シーケントの体系

• 式と推論
• 単純型付きラムダ

片側シーケントの古典論理が書いてある。ここだと、Gentzen-Shutte（ゲンツェン／シュッテ）になっている。ん？ ゲンツェン／テイトじゃなかった？

田中さんの言うGentzen-Taitシステムと、A.S.T and H.SのGentzen-Shutteシステムはどうも同じものらしい。Gentzen-Shutte-Taitといえば不公平はないかな。念のため、定義を書いておく。まず田中本より。

• atomic formulaまたはその否定を基本とする。Prologだと、これをリテラルと呼んでいた気がするが、半分忘れた。それと、否定を原子記号に組み込んで極性（polarity）付き記号を使う流儀もあったな、バーワイズがやっていたような、、、参考：「多圏上のシーケント計算」
• 一般のformulaは、∧、∨、∀、∃を結合子、限量子として組み立てる。
• 論理結合子としての否定は考えない。

φ, ψなどは論理式（formula）、αはリテラルだとする。リテラルに限って、¬αが許され、¬¬α = α とみなす。これは双対スターオペレータと同じ。

Tを論理式の集合とする。つまりTはセオリー（の生成系）。公理となるシーケントは：

• φ∈T に対して、⇒φ は公理
• ⇒α,¬α は公理

構造規則は：

換

   ⇒Γ

  -------

   ⇒Γ'  （Γ'はΓを適当に入れ替えたもの）

増

    ⇒Γ

  -------

   ⇒Γ,Δ

田中さんも A.S.T-H.S も換を入れる代わりにmultisetを使っているが。次に論理的規則：

   ⇒Γ,φ,ψ

  ------------- ∨導入

   ⇒Γ,φ∨ψ

   ⇒Γ,φ   ⇒Γ,ψ

  ------------------ ∧導入

     ⇒Γ,φ∧ψ


   ⇒Γ,φ(t)  （tは項）

  ---------------- ∃導入

   ⇒Γ,∃x.φ(x)


   ⇒Γ,φ(x) （xは変数で、Γに自由に出現しない）

  ------------- ∀導入

   ⇒Γ,∀x.φ
 

   ⇒Γ,¬α   ⇒Γ,α

  -------------------- cut

     ⇒Γ

A.S.T-H.Sでは、∨導入が左右2つある。

   ⇒Γ,φ

  ------------- ∨導入1

   ⇒Γ,φ∨ψ

   ⇒Γ,ψ

  ------------- ∨導入2

   ⇒Γ,φ∨ψ

換と増があれば、１つで十分。

それと、田中本では言及されてなかった減がある。multisetと考えればこれは不要。

   ⇒Γ,φ,φ

  ----------

   ⇒Γ,φ

cutは次の形。

   ⇒Γ,α   ⇒Δ,¬α

  -------------------- cut

     ⇒Γ,Δ

この違いも本質的ではない。