第 4 章 ラベル付きシークエント計算の体系 83
4.2 G3F(m) ∗ がカバーする体系
本節では，G3F(m)∗ がどの程度の範囲の論理体系をカバーすることができるのかにつ いて見る．
4.2.1 中間論理
中間論理は，直観主義論理と古典論理の間にある論理体系のことを指す．直観主義論理 の体系は，G3Fmを表 4.3の(Ref)と(T ran)を用いて拡張することによって手にでき る．この体系をここでは，G3Intと呼ぶ．直観主義論理のラベル付きシークエント計算
の体系は (Dyckhoff and Negri 2012)でも扱われている．しかし，この二つの体系には違
いがある． (Dyckhoff and Negri 2012)の体系は，命題変数の単調性の公理：
xRy, x:P,Γ⇒∆, y:P
を持つが，これは，G3Intで証明可能である．逆に，(Dyckhoff and Negri 2012)では，
G3Intの(Id)が導出可能であり，(M on)は許容可能である．そのため，G3Intとして ここで与える体系と，(Dyckhoff and Negri 2012)で与えられる直観主義論理のラベル付
第4章 ラベル付きシークエント計算の体系 94 きシークエント計算の体系はその証明力が変わらないことがわかる．
このとき，幾何学的含意図式を用いて，(Dyckhoff and Negri 2012)で行われているよ うに，幾つかの中間論理をカバーすることができる．
1 Jankov Logic KC：Jankov Logicあるいは弱排中律の論理は公理¬P ∨ ¬¬P に よって特徴づけらる．Jankov Logic のラベル付きシークエント計算 G3Janは Table 4.3の(Dir)をG3Intに加えれば良い．
2 G¨odel-Dummet Logic LC：G¨odel-Dummet Logic は公理 (P⊃Q) ∨(Q⊃P) に よって特徴付けられる．G¨odel-Dummet Logic のラベル付きシークエント計算 G3GDはTable 4.3の(Con)をG3Intに加えれば良い．
3 古典論理 G3CL：古典論理は，¬¬P⊃P か¬P ∨P を直観主義論理に加えること で特徴付けられる．古典論理のラベル付きシークエント計算G3CLはTable 4.3
の(Sym)か(Euc)（この二つはRの反射性が仮定されているときには互いに同値
になる）をG3Intに加えれば良い．
4.2.2 BPL の拡張
BPLでは，直観主義論理の定理である(P&(P⊃Q))⊃Qも(P⊃(P⊃Q))⊃(P⊃Q)も どちらも定理ではない． (Visser 1981)において初めて導入されたときには，BPLの体 系は自然演繹であったが，現在では，ゲンツェン流のシークエント計算の体系 (Ardeshir and Ruitenburg 1998, Ishii et al. 2001, Kikuchi and Sasaki 2003, Ruitenburg 1991)や ヒルベルト流の公理系(Kikuchi 2001, Suzuki and Ono 1997, Suzuki et al. 1998)が与え られている．ラベル付きシークエント計算のBPLの体系G3BPLは，G3FmをTable
4.3の(T ran)で拡張することによって手に入れることができる．このとき，G3BPLの
二つの拡張を与えることができる：
1. DNT：DNTはBPLに¬¬⊤を加えることで手にできる論理体系である (Ishi-gaki and Kashima 2008)．DNTのラベル付きシークエント計算の体系G3DNT はG3BPLにTable 4.3の(Ser)の規則を加えれば手にできる．
2. Log(•) (Ma and Sano 2015)：Table 4.3の空関係の条件によってBPLを拡張す ることによって手にできる．このとき，Log(•)のラベル付きシークエント計算は BPLにTable 4.3の(Emp)の規則を加えれば手にできる．
第4章 ラベル付きシークエント計算の体系 95
4.2.3 厳密含意論理
厳密含意の論理は，C. I. ルイスによって，実質含意のパラドクスを解消することを目 的として提案された (Lewis 1912)．厳密含意の幾つかの体系は， (Lewis 1913)の中で 初めて提示された．厳密含意論理の族に関しては， (Corsi 1987) の中で弱論理という名 で，その論理たちについての研究が行われており，ヒルベルト流の公理系が与えられた．
また， (Ishigaki and Kashima 2008)では，厳密含意のコルシの論理体系Fに対するラ ベルなしのゲンツェン流のシークエント計算の体系が与えられた． (Doˇsen 1993, Restall
1994)でも，厳密含意の論理たちに対するヒルベルト流の公理系が与えられている．さら
に，厳密含意論理の自然演繹の体系は (Cerrato 1994)において与えられている．
厳密含意論理はときに，部分直観主義論理と呼ばれることがある．この部分直観主義 論理はクリプキモデルのクラスによって特徴付けられる．厳密含意論理のクリプキモデ ルは直観主義論理のクリプキモデルとその充足条件は同じであるが，単調性はいつも成 り立つとは限らない．厳密含意論理はフレーム条件の組み合わせとして扱うことができ る．では以下で，先行研究などで扱われている厳密含意論理の拡張した体系の幾つかを，
G3F(m)∗ を用いて扱うことができることについて見る．
1. FD：FD (Corsi 1987)はFに¬¬⊤ を付け加えることで手にでき，継起性を満 たすクリプキモデルのクラスによって特徴付けられる．この論理は Dσ (Doˇsen 1993) として，GKDI (Ishigaki and Kashima 2008) として，研究されている．
FDのラベル付きシークエント計算の体系G3FDはG3FにTable 4.3の(Ser) の規則を加えれば手にできる．
2. FC：FC (Corsi 1987)はFに公理((C&(A⊃B))⊃D)∨((A&(C⊃D))⊃B)を付 け加えることで手にできる．FCのラベル付きシークエント計算G3FCはG3F にTable 4.3の(Con)の規則を加えれば手にできる．
3. FT：FT (Corsi 1987)はFに公理(A⊃B)⊃(C⊃(A⊃B))を付け加えることで手 にできる．また， (Ishigaki and Kashima 2008)においてラベルなしのシークエ ント計算GK4I が与えられている．また， (Restall 1994)では，bという名前で その体系が与えられている．FTのラベル付きシークエント計算の体系G3FTは G3FにTable 4.3の(T ran)の規則を加えれば手にできる．
4. FR：FR (Corsi 1987)はFに公理A&(A⊃B)⊃Bを付け加えることで手にでき る．また，(Ishigaki and Kashima 2008)においてラベルなしのシークエント計算
第4章 ラベル付きシークエント計算の体系 96 GKTI が与えられている．FRのラベル付きシークエント計算の体系G3FRは G3FにTable 4.3の(Ref)の規則を加えれば手にできる．
5. FRT：FRT (Corsi 1987)はFTに公理A&(A⊃B)⊃Bを付け加えることで手に できる． (Ishigaki and Kashima 2008)においてラベルなしのシークエント計算 GKS4Iが与えられている．また，(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)においてラベルなしのシークエント計算 GKBI が与えられている．FRSのラベル付きシークエント計算の体系G3FSは G3FにTable 4.3の(Ser)の規則を加えれば手にできる．(Ishigaki and Kashima
2008)の中で，GKBI のカット規則の許容可能性は示されていないが，のちに見
るように，G3FSにおいてカット規則が許容可能であることが示される．
7. GK5I：GK5I (Ishigaki and Kashima 2008)はユークリッド性でそのフレーム 条件が特徴付けられるような論理体系のラベルなしのシークエント計算の体系で ある．GK5I のラベル付きシークエント計算の体系G3FEはG3FにTable 4.3 の(Euc) の規則を加えれば手にできる． (Ishigaki and Kashima 2008) の中で，
GK5Iのカット規則の許容可能性は示されていないが，G3FEにおいてカット規 則が許容可能であることが示される．
ラベル付きシークエント計算を用いて形式化したときには，各論理体系の違いは，ベー スとなるG3Fに，フレームに関するどの規則を加えるかの違いに依存して決まる．この ようにして，様々な論理体系を一様な仕方で与える手法は，現在多くの形式体系で採用さ れており，例えば，ハイパーシークエントやツリーシークエントなどがある*3．