構造規則を吸収した体系

第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) .

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

第2章 シークエント計算とその発展 43 消滅したのかはわからない．そのため，カット規則の適用が許されているときには，一般 にはその証明図の構成は格段に難しくなる，つまり，証明探索が困難になるということで ある．これと同じことが，弱化と縮約の規則の場合にも生じる．そのため，その性質から して，構造規則を持っている方が望ましい論理体系に対して，構造規則の機能は維持しつ つ，しかし，明示的にそれらの規則は含まれていない形式体系を与えることが可能である ことが望ましい．この点に主眼を置いて発展したと考えられる形式体系の一つが，G3型 と呼ばれるタイプのシークエント計算である^*6．G3型で形式化されたシークエント計算 では，構造規則が形式体系の中に吸収されている．つまり，証明図を構成する際に明示的 に構造規則が用いられることはないが，その働きは他の結合子の推論規則の中に組み込ま れているのである．このとき，構造規則を吸収した体系を用いて証明できる命題たちの集 合の範囲は，構造規則を明示的に用いて証明を行う場合とその範囲を変えない．では以下 で，G3型のシークエント計算がどのような形式体系であり，今述べたことがどのように 実現されているのかについて，直観主義論理のシークエント計算の体系を例にとってその 説明を行う．

LJをはじめとする直観主義論理のシークエント計算の体系では，伝統的には，シーク エントの後件では，論理式の出現がただ一つに制限されたものが用いられる．しかし，こ こでは，その条件を取り除いて，直観主義論理のシークエントであっても，シークエント の後件に出現する論理式は複数個で構わないものを用いる．直観主義論理の後件複数な 形での形式化は様々に行われているが，ここでは，表 2.3のように与えられる形式体系 G3I^{を用いる*7．}G3I^は， (Troelstra and Schwichtenberg 2000, Negri and von Plato

2001)などの様々な文献の中で触れられている^*8*9．

*6G3^{型については}(Troelstra and Schwichtenberg 2000, Negri and von Plato 2001)^{に詳しい．}

*7直観主義論理の後件が複数な形のシークエント計算の体系は，本論で扱うもの以外にも(Negri and von Plato 2001)などで提案されているものもある． (Negri and von Plato 2001)^では，G3I^と，(L⊃) の規則が異なる．(Negri and von Plato 2001)^での(L⊃)^{の規則は以下：}

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

.

*8また，(Troelstra and Schwichtenberg 2000, p.88)において，A.ドラガリンがH. A. J. M.シュリ ネックスに宛てた手紙（1990.11.22.^{）の中で，自身の} (Dragalin 1988)の中で用いた含意の左規則よ り，G3型の直観主義論理の後件複数なシークエント計算の規則としては，ここで与えたG3I^の左規則 の方が好ましいとい考えていたということが述べられている．その理由の一つとして，この規則の高さ保 存の反転可能性が両方の前提に対して成立するということが挙げられている．

*9また，G3Iに対する，G3型でない直観主義論理の後件複数なシークエント計算の体系は，(Maehara

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

表2.3 G3I (Axioms)

P,Γ⇒∆, P (Id)

⊥,Γ⇒∆ (L⊥) (Logical rules)

A, B,Γ⇒∆

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

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

Γ⇒∆, A∨B (R∨)

A⊃B,Γ⇒∆, A B,Γ⇒∆

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

Γ⇒∆, A⊃B (R⊃)

先にも述べたように，G3型のシークエント計算の体系は，弱化，縮約，カット規則が 論理結合子の推論規則の中に吸収されているのであるが，それがどのように実現されてい るのかを以下で見る．この点について確認するため，まずはじめに必要な定義^*10を与え，

その準備を行う．

まずは，主式についての定義である．

定義 24 (文脈，主式). G3Iの推論規則におけるΓと∆は文脈（context）と呼ばれる．

G3I の各規則の結論において，文脈に含まれていない論理式（たち）は主式（principal formula (s)）と呼ばれる．

次は，導出についての用語法である．

定義 25 (^導出). G3I^{における導出（}derivation^） D^は公理とG3I^{の規則によって生成} される有限木構造として帰納的に定義される．D のルートノードにあるシークエントを D^{のエンドシークエント（}end sequent）と呼ぶ．導出の高さは，エンドシークエントから 公理に至るまでの導出の中での極大な枝の長さとする．もし，Γ⇒ ∆がそのエンドシー

1954)で，L^′Jとして，扱われている．

*10ここでの定義は，G3型のシークエント計算を用いたカット除去定理を行うために与えるものである．

G3型のシークエント計算を用いたカット除去定理の議論は，ラベルなしのシークエント計算について は (Troelstra and Schwichtenberg 2000, Negri and von Plato 2001)などで，ラベル付きシークエ ント計算については，(Negri 2005, Dyckhoff and Negri 2012, Yamasaki and Sano 2016)^などで扱 われている．

第2章 シークエント計算とその発展 45 クエントがΓ⇒∆であるようなG3Iにおける導出D^{を持つなら，}Γ⇒∆はG3Iにお いて導出可能（derivable）である（G3I⊢Γ⇒∆と書く）．Γ⇒∆の証明図の高さがせ いぜいnであることをG3I⊢n Γ⇒∆と書く．

もしも，そのことが記述の文脈から明らかな場合には，しばしば“G3I⊢Γ⇒∆”とい う表現から“G3I”を省略する．今，G3Iでは，複合式の同一性が成り立つ．

命題 2 (複合式の同一性). 任意の論理式 A に対して，A,Γ ⇒ ∆, A のような形をした シークエントがG3Iで導出可能である．

次は，証明図の高さを保存した，推論規則の許容可能性についての定義である．

定義 26 (許容可能性). G3Iにおいて，ある規則の前提が導出可能であるときにはいつで も，もしその規則の結論もG3Iにおいて導出可能であるなら，その規則は，G3Iにおい て，許容可能（admissible）と言われる．

G3Iにおいて，ある規則の，前提がせいぜい高さnで導出可能であるときにはいつでも，

もし，その規則の結論もG3Iにおいて，せいぜい高さnで導出可能であるなら，その規則 は，G3Iにおいて，高さ保存で許容可能（height-preserving admissible, hp-admissible） と言われる．

この定義の下で，弱化は高さ保存で許容可能である．弱化の規則は，

Γ⇒∆

A,Γ⇒∆ (LW) Γ⇒∆

Γ⇒∆, A (RW) の二つ．

補題 3 (弱化の許容可能性). 弱化の規則はG3Iで，高さ保存で許容可能である：

(i) もし⊢nΓ ⇒∆なら，そのとき，⊢nA,Γ⇒∆． (ii) もし⊢nΓ ⇒∆なら，そのとき，⊢nΓ⇒∆, A． 次は反転可能性についての定義である．

定義 27 (反転可能性). G3Iにおいて，ある規則の，結論がせいぜい高さnで導出可能で あるときにはいつでも，その規則の前提もG3Iにおいて，せいぜい高さn^{で導出可能であ} るなら，その規則は，G3Iにおいて，高さ保存で反転可能（height-preserving invertible, hp-invertible）と言われる．

第2章 シークエント計算とその発展 46 このとき，G3Iでは，次のことが成り立つ．

補題 4 (反転可能性). G3Iの(R⊃)規則以外のすべての規則は，高さ保存で反転可能．

補題 5 (縮約の許容可能性). 縮約の規則は，G3Iで高さ保存で許容可能：

(i) もし，⊢nA, A,Γ ⇒∆なら，そのとき⊢n A,Γ⇒∆． (ii) もし，⊢nΓ ⇒∆, A, Aなら，そのとき，⊢n Γ⇒∆, A． 続いては，カット規則の許容可能性についてである．

命題 6 (G3Iのカット規則の許容可能性). (Cut)の規則：

Γ⇒∆, A A,Π ⇒Σ

Γ,Π⇒∆,Σ (Cut) はG3Iにおいて許容可能である（カット除去可能である）．

このようにして，G3型のシークエント計算では，構造規則がその形式体系内に吸収さ れる．そのため，シークエント計算をG3型の形に変形することができれば，その証明探 索の労力は格段に低くて済むのである．

さて，では次にG. ミンツによって与えられた直観主義論理の後件複数な体系の一つで あるLJpmを見る．ここでは，LJpmを用いて，形式体系からモデルを構成するという 操作がどのような手順で行われるのかについて見る．