LK と LJ

ゲンツェンは，1935^年に“Untersuchungen ¨uber das logische Schliessen”^{において自} 然演繹とシークエント計算を与えた．自然演繹では論理結合子に対する除去則と導入則と が与えられ，結合子の意味が定められる．自然演繹はその名の通り，人間の自然な推論

（actual reasoning）を形式化した体系と言われている（cf. (Gentzen 1935), p.68 ）．一 方，シークエント計算は，証明図の構成という点に目下の主眼を置き，与えられた体系で ある．では以下で，シークエント計算の体系を説明するために必要な用語の導入から始め る．語彙，論理式，シークエントの定義は，定義 1，定義 2，定義 22とそれぞれ同じで 良い．

表2.1によって与えられるのが，古典論理のシークエント計算の体系LKである．この とき，直観主義論理のシークエント計算の体系LJ（表 2.2）はLKにおいて，シークエ ントの後件に出現する論理式の数をたかだか一つに制限すれば手にできる．

本論ではその詳しい証明は見ないが，LKとLJでは，カット除去定理が成り立つ．

第2章 シークエント計算とその発展 40

表2.1 LK (Gentzen 1935) (Axioms)

A⇒A (Id) (Logical Rules)

A0,Γ⇒∆

A₀&A₁,Γ⇒∆ (L&) A1,Γ⇒∆

A₀&A₁,Γ⇒∆ (L&) Γ⇒∆, A Γ⇒∆, B

Γ⇒∆, A&B (R&) A,Γ ⇒∆ B,Γ⇒∆

A∨B,Γ⇒∆ (L∨) Γ⇒∆, A0

Γ⇒∆, A0∨A1

(R∨) Γ⇒∆, A1

Γ ⇒∆, A0∨A1

(R∨) Γ ⇒∆, A B,Θ⇒Ξ

A⊃B,Γ,Θ⇒∆,Ξ (L⊃) A,Γ ⇒∆, B

Γ⇒∆, A⊃B (R⊃)

Γ⇒∆, A

¬A,Γ⇒∆ (L¬) A,Γ⇒∆

Γ⇒∆,¬A (R¬) (Structural Rules)

A, A,Γ⇒∆

A,Γ⇒∆ (LC) Γ⇒∆, A, A

Γ⇒∆, A (RC)

Γ⇒∆

A,Γ⇒∆ (LW) Γ⇒∆

Γ⇒∆, A (RW)

Γ, B, A,Σ⇒∆

Γ, A, B,Σ⇒∆ (LE) Γ⇒Σ, B, A,∆

Γ⇒Σ, A, B,∆ (RE) Γ⇒∆, A A,Σ⇒Π

Γ,Σ⇒∆,Π (Cut)

Fact 1 (LKとLJのカット除去定理). Γ⇒∆を終式とするLK証明図に対し，これと 同じ終式を持ち，かつカット規則を含まないような証明図を作ることができる．このこと は，LJに対しても成り立つ．

また，LKと，第1章で与えた，古典論理のヒルベルト流の公理系との間に次のような 対応関係が成り立つ．ここでまず，Γ≡A₀, . . . , A_mのとき，Γの要素を全て&で繋いだ 論理式∧

Γと，Γの要素を全て∨^{で繋いだ論理式}∨

Γを以下のように定める．

第2章 シークエント計算とその発展 41

表2.2 LJ(Gentzen 1935) (Axioms)

A⇒A (Id) (Logical Rules)

A0,Γ⇒∆

A₀&A₁,Γ⇒∆ (L&) A1,Γ⇒∆

A₀&A₁,Γ ⇒∆ (L&) Γ⇒A Γ⇒B

Γ⇒A&B (R&) A,Γ⇒∆ B,Γ⇒∆

A∨B,Γ⇒∆ (L∨) Γ⇒A0

Γ⇒A0∨A1

(R∨) Γ⇒A1

Γ ⇒A0∨A1

(R∨) Γ⇒A B,Θ⇒Ξ

A⊃B,Γ,Θ⇒Ξ (L⊃) A,Γ ⇒B

Γ⇒A⊃B (R⊃)

Γ⇒A

¬A,Γ ⇒ (L¬) A,Γ⇒

Γ⇒ ¬A (R¬) (Structural Rules)

A, A,Γ⇒∆ A,Γ⇒∆ (LC)

Γ ⇒∆

A,Γ⇒∆ (LW) Γ⇒

Γ⇒A (RW)

Γ, B, A,Σ⇒∆ Γ, A, B,Σ⇒∆ (LE) Γ⇒A A,Σ⇒∆

Γ,Σ⇒∆ (Cut)

定義 23.

∧Γ =

{A1∧. . .∧Am m >0のとき

⊤ m= 0のとき

∨Γ = {

A1∨. . .∨Am m >0のとき

⊥ m= 0のとき

Fact 2. シークエントΓ ⇒∆を論理式 ∧ Γ⊃∨

∆へと翻訳する．このとき，次のこと が成り立つ．

第2章 シークエント計算とその発展 42

LK⊢ Γ⇒∆ ⇔ ⊢HK

∧Γ⊃∨

∆

このことは，LJと直観主義論理のヒルベルト流の公理系との間にも成り立つ．

LK^やLJはシークエント計算の最も基本となる形式体系であり，現在では，様々に改 良されたシークエント計算の形式体系が与えられている．以下では，その幾つかについて 見ることで，シークエント計算についてさらに掘り下げていく．

ところで，本章の冒頭で述べた，LKでの排中律の証明図は以下のように与えられる：

P ⇒P (Id)

⇒P,¬P (R¬)

⇒P ∨ ¬P,¬P (R∨)

⇒P ∨ ¬P, P ∨ ¬P (R∨)

⇒P ∨ ¬P (RC) .

このとき，後件に論理式が二つ以上出現している箇所がある．そのため，シークエント の後件に論理式がたかだか一つしか出現することのできない直観主義論理では，排中律を 示すことができないのである．