G3F(m) ∗ のカット除去定理

第4章 ラベル付きシークエント計算の体系 96 GKT^I が与えられている．FRのラベル付きシークエント計算の体系G3FRは G3FにTable 4.3の(Ref)の規則を加えれば手にできる．

5. FRT：FRT (Corsi 1987)はFTに公理A&(A⊃B)⊃Bを付け加えることで手に できる． (Ishigaki and Kashima 2008)においてラベルなしのシークエント計算 GKS4^Iが与えられている．また，(Restall 1994)^では，bw^{という名前でその体系} が与えられている．FRTのラベル付きシークエント計算の体系G3FRTはG3F にTable 4.3の(Ref)と(T ran)の規則を加えれば手にできる．

6. FS：FS (Corsi 1987)はF に公理 A⊃(B∨ ¬(A⊃B))を付け加えることで手に できる． (Ishigaki and Kashima 2008)においてラベルなしのシークエント計算 GKB^I が与えられている．FRSのラベル付きシークエント計算の体系G3FSは G3FにTable 4.3の(Ser)の規則を加えれば手にできる．(Ishigaki and Kashima

2008)の中で，GKB^I のカット規則の許容可能性は示されていないが，のちに見

るように，G3FSにおいてカット規則が許容可能であることが示される．

7. GK5^I：GK5^I (Ishigaki and Kashima 2008)はユークリッド性でそのフレーム 条件が特徴付けられるような論理体系のラベルなしのシークエント計算の体系で ある．GK5^I のラベル付きシークエント計算の体系G3FEはG3FにTable 4.3 の(Euc) の規則を加えれば手にできる． (Ishigaki and Kashima 2008) の中で，

GK5^Iのカット規則の許容可能性は示されていないが，G3FEにおいてカット規 則が許容可能であることが示される．

ラベル付きシークエント計算を用いて形式化したときには，各論理体系の違いは，ベー スとなるG3Fに，フレームに関するどの規則を加えるかの違いに依存して決まる．この ようにして，様々な論理体系を一様な仕方で与える手法は，現在多くの形式体系で採用さ れており，例えば，ハイパーシークエントやツリーシークエントなどがある^*3．

第4章 ラベル付きシークエント計算の体系 97

z[y/x] ≡

{y if z ≡x;

z if z ̸≡x.

また，以下のようにして，ラベル付き表現φ^{において，代入}[y/x]^{を自然な形で定義で} きる：

(z:A)[y/x]≡z[y/x] :Aかつ(zRw)[y/x]≡z[y/x]Rw[y/x].

補題 25 ( (Yamasaki and Sano 2016, Lemma 1)). もし，Γ ⇒∆がG3F(m)^∗ におい て導出可能であるなら，そのとき，Γ[y/x]⇒∆[y/x]も，高さ保存で導出可能である．つ まり，もし，G3F(m)^∗ ⊢nΓ ⇒∆なら，そのとき，G3F(m)^∗ ⊢n Γ[y/x]⇒∆[y/x].

この補題 25を高さ保存の代入（height-preserving substitution, hp-substitution）と 呼ぶ．

定義 49 (許容可能性, (Yamasaki and Sano 2016, Definition 6)). G3F(m)^∗ において，

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

G3F(m)^∗ において，その規則の，前提がせいぜい高さnで導出可能であるときには いつでも，もし，その規則の結論もG3F(m)^∗ において，せいぜい高さnで導出可能で あるなら，その規則は，G3F(m)^∗ において，高さ保存で許容可能（height-preserving admissible, hp-admissible）と言われる．

補題 26 (弱化の許容可能性, (Yamasaki and Sano 2016, Lemma 8)). 弱化の規則は G3F(m)^∗ で高さ保存で許容可能である．つまり：

(i) もし，⊢nΓ ⇒∆なら，そのとき，⊢nx:A,Γ⇒∆.

(ii) ^もし，⊢nΓ ⇒∆^{なら，そのとき，}⊢nΓ ⇒∆, x:A.

(iii) もし，⊢nΓ ⇒∆なら，そのとき，⊢nxRy,Γ⇒∆.

この補題の各項は導出の高さnについての帰納法を用いて示すことができる．

定義 50 (反転可能性, (Yamasaki and Sano 2016, Definition 7)). G3F(m)^∗ において，

その規則の，結論がせいぜい高さnで導出可能であるときにはいつでも，もし，その規 則の前提もG3F(m)^∗ において，せいぜい高さnで導出可能であるなら，その規則は，

G3F(m)^∗ において，高さ保存で反転可能（height-preserving invertible, hp-invertible）

第4章 ラベル付きシークエント計算の体系 98 と言われる．

補題 27 (反転可能性, (Yamasaki and Sano 2016, Lemma 3)). G3F(m)^∗の全推論規則 は，高さ保存で反転可能である.

補題 28 (縮約の許容可能性, (Yamasaki and Sano 2016, Lemma 4)). 縮約の規則は，

G3F(m)^∗ において高さ保存で許容可能である．つまり：

(i) ^もし，⊢nx:A, x:A,Γ⇒∆^{なら，そのとき，}⊢n x:A,Γ ⇒∆.

(ii) もし，⊢nΓ ⇒∆, x:A, x:Aなら，そのとき，⊢n Γ⇒∆, x:A.

(iii) もし，⊢nxRy, xRy,Γ⇒∆なら，そのとき，⊢n xRy,Γ⇒∆.

定義 51 ( (Yamasaki and Sano 2016, Definition 8)). ラベル付きカット式x:Aの重さ

（weight^）は，Aにおける論理結合子の数とする．また，(Cut)^の高さ（cut-height^）は，

(Cut)の二つの前提の導出の高さの和とする．

定 理 8 (G3F(m)^∗ の カ ッ ト 除 去 定 理, (Yamasaki and Sano 2016, Theorem 1)).

G3F(m)^∗ においてカット規則は許容可能．

Proof. ^{ラベル付きカット式}x:Aの重さについての帰納法と，(Cut)^のcut-height^につい ての部分帰納法を用いて示す．まず，以下に挙げる(i)と(ii)の場合を考える．このとき，

カットの前提の少なくとも一つが公理か前提なしの幾何学的規則図式である．残りの場合 に対しては，三つの場合分けが存在する：(iii) 左の前提では，カットラベル付き表現は主 式ではない；(vi) 左の前提だけで，カットラベル付き表現が主式；(v) カットの前提の両 方でカットラベル付き表現が主式．

(i) カットの左の前提が公理か幾何学的規則図式：この場合の証明は省略する．

(ii) カットの右の前提が公理か幾何学的規則図式：まず，右の前提x:A,Π ⇒ Σが公 理(Id)であると仮定する．つまり，以下の場合のうちの一つを手にしているとす る：右の前提が次の形x:A, y:P,Π^′ ⇒ Σ^′, y:P かx:P,Π ⇒ Σ^′, x:P をしていると き．後者の場合には A ≡ P であり，前者の場合には，Γ,Π ⇒ ∆,Σも公理(Id) となる．後者の場合，Γ,Π ⇒ ∆,Σ^′, x:P を手にできる．これは，高さ保存の弱 化の規則の適用を行うことによって，左の前提Γ ⇒ ∆, x:P から導くことができ る．次に，右の前提が公理(L⊥)であると仮定する．もし，カットラベル付き表現 x:AにおいてA ̸≡ ⊥^{であるとき，}Π中にw:⊥が含まれる．そういうわけなので，

第4章 ラベル付きシークエント計算の体系 99 Γ,Π ⇒∆,Σも公理(L⊥)である．そうでない場合，つまり，もし，A ≡ ⊥^である とき，左の前提Γ⇒∆, x:⊥の最後の規則を調べる必要がある．もし，最後の規則 が公理の場合，この場合は(i)の場合へと還元できる．それ以外の場合には，(iii) の特別な場合となる．

最後に，右の前提が前提なしの幾何学的規則図式であると仮定する．もし，カット の右の前提がx:A, S,Π^′ ⇒ Σなる形をした前提なしの幾何学的規則図式であると き，カットの結論も前提なしの幾何学的規則図式である．

(iii) カットラベル付き表現が左の前提で主式でない：ここでは，(Cut)の左の前提の

最後に適用された規則に依存して場合分けを行う．つまり，すべての推論規則と

(M on)と(GRS)の場合を含めて八つの場合分けが考えられる．ここでは，(R⊃)

の場合を考える．このとき，以下の導出が考えられる：

.. ..

yRz, z:B,Γ⇒∆^′, z:C, x:A

Γ⇒∆^′, y:B⊃C, x:A (R⊃)†

.. .. x:A,Π⇒Σ Γ,Π⇒∆^′, y:B⊃C,Σ (Cut)

,

ここでは，zはより下のシークエントΓ ⇒∆^′, y:B⊃C, x:Aの中に出現しない．ま ず，変項の衝突を避けるために，yRz, z:B,Γ⇒∆^′, z:C, x:Aに対して，[w/z]を用 いて，高さ保存の代入を行う．ここでは，w^は(Cut)の結論中には存在しないと仮 定する．このとき，以下の導出を手にすることができる：

.. ..

yRw, w:B,Γ⇒∆^′, w:C, x:A

.. .. x:A,Π⇒Σ yRw, w:B,Γ,Π⇒∆^′, w:C,Σ (Cut)

Γ,Π⇒∆^′, y:B⊃C,Σ (R⊃)† ,

今，cut-heightが最初より下がっているので，カット規則の適用が可能となる．こ

れ以外の場合にも（(GRS)と(M on)も含むが），同様の仕方で示すことができる．

また特に，固有変項条件のない推論規則の場合（例えば，(M on)）には，ここで示 したよりも簡単に示すことができる．

(iv) 左の前提だけで，ラベル付きカット表現が主式：ここでは，(Cut)の右の前提で最 後に適用された規則によって場合分けを行う．しかし，最初の場合分けの条件付け から，右の前提の最後に適用された規則において，カットラベル付き表現x:Aは主 式ではない．この場合の議論は (iii)と同様の仕方で示すことができるため，その 証明は省略する．

第4章 ラベル付きシークエント計算の体系 100 (v) カットラベル付き表現がカットの両方の前提で主式：このとき，さらに三つの場合

分けが生じる：カットラベル付き表現x:Aにおいて，AがB∨CかB&CかB⊃C である場合の3つである．私たちは次のような導出を手にできる：

.. ..

xRz, z:B,Γ⇒∆, z:C

Γ⇒∆, x:B⊃C (R⊃)†

.. ..

x:B⊃C, xRw,Π⇒Σ, w:B

.. ..

w:C, x:B⊃C, xRw,Π⇒Σ x:B⊃C, xRw,Π⇒Σ (L⊃)

xRw,Γ,Π⇒∆,Σ (Cut)

, ここでz はより下のシークエントΓ ⇒ ∆, x:B⊃C には出現しない．このとき，

[w/z]に対する高さ保存の代入を用いて，以下のようなDLなる導出を構成できる：

.. .. Γ⇒∆, x:B⊃C

.. ..

x:B⊃C, xRw,Π⇒Σ, w:B xRw,Γ,Π⇒∆,Σ, w:B (Cut)

.. ..

w:B, xRw,Γ⇒∆, w:C xRw, xRw,Γ,Γ,Π⇒∆,∆,Σ, w:C (Cut)

, ここでは，cut-heightが低くなっているため，左のカット規則の適用が可能であ ること，カットラベル付き表現w:B の重さはx:B⊃C の重さより下がっているた め，カット規則の最後の適用が可能となる．

次に，もとの導出から以下のような導出DRも構成することができる：

.. ..

xRz, z:B,Γ⇒∆, z:C Γ⇒∆, x:B⊃C (R⊃)

.. ..

x:B⊃C, w:C, xRw,Π⇒Σ w:C, xRw,Γ,Π⇒∆,Σ (Cut)

,

ここでは，cut-heightが下がっているので，カット規則の最後の適用が可能であ ることに注意しなければならない．今，私たちはDLとDRによって次の導出を手 にできる：

DL

xRw, xRw,Γ,Γ,Π ⇒∆,∆,Σ, w:C DR

w:C, xRw,Γ,Π ⇒∆,Σ

xRw, xRw, xRw,Γ,Γ,Γ,Π,Π⇒∆,∆,∆,Σ,Σ (Cut)

xRw,Γ,Π⇒∆,Σ ,

ここでは，証明図中の二重線は縮約を必要な回数適用することを示している．ま た，カットラベル付き表現w:C の重さがx:B⊃C の重さより下がっているため，

カット規則の適用が可能となる．

第4章 ラベル付きシークエント計算の体系 101