BPL の G3 型のラベルなしのシークエント計算

表 3.1で，私たちは，BPLのG3型のラベルなしのシークエント計算の体系（G3B） を与える．ここでまず，含意に対する規則(⊃)の例を幾つか与えよう．n = 0,1,2のと き，規則の形は以下のようになる：

Σ, A⇒B

Σ⇒A⊃B,Θ (⊃) ,

Σ, C₁⊃D₁, A ⇒B, C₁ D₁, C₁⊃D₁,Σ, A ⇒B Σ, C1⊃D1 ⇒A⊃B,Θ (⊃)

,

Σ,Φ, A ⇒B, C1, C2 D1,Σ,Φ, A ⇒B, C2 D2,Σ,Φ, A⇒B, C1 D1, D2,Σ,Φ, A⇒B Σ, C₁⊃D₁, C₂⊃D₂ ⇒A⊃B,Θ (⊃)

, ここでは，Φ≡C₁⊃D₁, C₂⊃D₂.

弱化と縮約などの構造規則はG3Bの中には見つけられないが，これらの規則は，次の 節で許容可能であることが示される．つまり，これらの規則を新しく加えることになって も，導出可能なシークエントの全体は変わらないということである．このとき，G3Bで の部分式特性はすぐに示せる．

命題 11 ( (Yamasaki and Sano 2017, Proposition 1)). G3B は部分式特性を満たす．

つまり，もしΓ ⇒ ∆ がG3Bで導出可能なら，シークエント Γ ⇒ ∆の部分論理式に よってそのシークエントの全てが構成されている．

G3Bは(⊃)規則に注意する必要があるため，改めてBPLでの文脈と主式の定義を与 えておく．

定義 36 (文脈，主式). (⊃)を除くG3Bの推論規則に含まれるΓと∆は文脈（context） と呼ばれる．(⊃)の規則においては，ΣとΘが文脈．G3Bの各規則の結論において，文 脈に含まれない論理式（たち）のことを主式（principal formula(s)）と呼ぶ．

第3章 ラベルなしのシークエント計算を用いたBPLとK4の埋め込み定理 60

表3.1 G3B (Yamasaki and Sano 2017) (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∨)

C1⊃D1, . . . , Cn⊃Dn,∆1,Σ, A⇒B,Γ1 . . . C1⊃D1, . . . , Cn⊃Dn,∆2ⁿ,Σ, A⇒B,Γ2ⁿ

Σ, C1⊃D1, . . . , Cn⊃Dn ⇒A⊃B,Θ (⊃)†

†: n≥0, Γ_i ={C_j | j ∈γ(i)}, ∆_i ={D_j | j ∈δ(i)}, 1⩽i⩽2ⁿ, かつ γ(i)は{1, . . . , n}の部分集合の上を走る．また，δ(i) ={1, . . . , n}∖γ(i)．

定義 37 (導出). G3Bにおける導出（derivation） D^は公理とG3Bの規則によって生 成される有限木構造として帰納的に定義される．Dのルートノードにあるシークエントを D^{のエンドシークエント（}end sequent）と呼ぶ．導出の高さは，エンドシークエントから 公理に至るまでの導出の中での極大な枝の長さとする．もし，Γ⇒ ∆^{がそのエンドシー} クエントがΓ ⇒∆であるようなG3Bにおける導出D^{を持つなら，}Γ⇒∆はG3Bに おいて導出可能（derivable^{）である（}G3B ⊢Γ ⇒ ∆^{と書く）．}Γ ⇒∆^{の証明図の高さ} がせいぜいnであることをG3B⊢n Γ⇒∆と書く．

命題 12( (Yamasaki and Sano 2017, Proposition 2)). 任意のAについて，A,Γ⇒∆, A なるシークエントがG3Bで導出可能である．

Proof. Aの複雑度についての帰納法で示す．もし，A^{が原子式か}⊥^{のときには明らか．}

もし，n >0なら，帰納法の仮定を適用することによって全ての場合を簡単に示すことが できる．ここでは，含意の場合のみ示す．もしA ≡B⊃C のとき，導出の最後のステッ プは以下のようになる：

第3章 ラベルなしのシークエント計算を用いたBPLとK4の埋め込み定理 61

....

B⊃C,Γ, B⇒C,∆, B

....

C, B⊃C,Γ, B ⇒C,∆ B⊃C,Γ⇒∆, B⊃C (⊃)

,

このとき，B⊃C,Γ, B ⇒ C,∆, BとC, B⊃C,Γ, B ⇒ C,∆は明らかに帰納法の仮定に よって導出可能であることがわかる．

(Ishii et al. 2001)においてもBPLのカットなしのシークエント計算の体系が与えら れており，“LBP” と呼ばれている（表 3.2を見よ）．

表3.2 LBP (Ishii et al. 2001) (Axioms)

A ⇒A ⊥ ⇒ (Inference Rules)

Γ⇒∆

A,Γ⇒∆ (LW) Γ⇒∆

Γ⇒∆, A (RW)

A, B,Γ⇒∆

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

Γ⇒∆, A&B (R&)

A,Γ⇒∆ B,Γ⇒∆

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

Γ⇒∆, A∨B (R∨)

∆1,Σ, A ⇒B,Γ1 . . . ∆2ⁿ,Σ, A⇒B,Γ2ⁿ

Σ, C₁⊃D₁, . . . , C_n⊃D_n⇒A⊃B (⊃)†

†: n≥0, Γi ={Cj | j ∈γ(i)}, ∆i ={Dj | j ∈δ(i)}, 1⩽i⩽2ⁿ, かつ γ(i)は{1, . . . , n}の部分集合の上を走る．また，δ(i) ={1, . . . , n}∖γ(i).

(Ishii et al. 2001)において，シークエントは論理式の有限集合のペアとして定義され

ていることに注意する必要がある．したがって，彼らの体系は，縮約（また，交換）の規 則を持たない．LBPの公理の形は，G3Bとは異なっている．&と∨^の規則はG3Bの 規則と同じである．しかし，含意の規則は，G3Bの規則と同じではない．LBPの含意

第3章 ラベルなしのシークエント計算を用いたBPLとK4の埋め込み定理 62 の規則と，G3Bの含意の規則を比較したとき，LBPの含意の規則は G3Bでの規則よ り，簡単な形をしている．これは，G3Bでは，弱化と縮約の規則が許容可能であること による．

LBPに対する，文脈，主式，導出の概念は，G3Bと同じである．後ほど，G3Bが LBPと同値であることを示す．