非様相論理のラベル付きシークエント計算の体系 G3F(m) ∗

非様相論理のラベル付きシークエント計算の諸体系は，G3Fをベースとして与えるこ とができる．このベースとなる G3Fに対し，目標とする論理体系がどのような性質を 持っているのかということに合わせて，必要な推論規則を加えていけば良い．このとき，

当該の論理体系のクリプキモデルを考えたときに，どのような条件が課されているのかと いうことを参考にすることで，必要な推論規則が何であるかを明らかにすることができ る．そのため，考えなければならないのは，二項関係xRyが持つ性質と，単調性について である．このことを踏まえて，ラベル付きシークエント計算では，二項関係xRyと単調 性についての規則を考える必要が生じてくる．何か欲しい論理体系がある時は，その体系 のクリプキモデルを参照し，そこでのフレーム条件として何が課されていたかを考え，必 要なRに関係する規則を先のG3Fに加えていけば良い．その具体的な手順については，

後ほど説明する．その準備として，まず本論内で必要となるRと，単調性についての規則 を与える．最初は，単調性の規則である．以下に与えるものが単調性を表す規則である：

xRy, x:P, y:P,Γ⇒∆

xRy, x:P,Γ⇒∆ (M on) .

この規則は，状態x^でP ^{が成り立ち，}x^からyへと情報が進展すると考えたとき，状態 y でP が成り立つという推論実践を記述していると考えられる．この性質は，単調性に

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

表4.2 幾何学的含意の例

性質の名前 フレーム条件

反射性（Reflexivity） ∀x(xRx)

推移性（Transitivity） ∀x, y, z(xRy&yRz ⊃xRz) 推移性（Symmetry） ∀x, y(xRy ⊃yRx)

連結性（Connectedness） ∀x, y, z((xRy&xRz)⊃(yRz∨zRy)) 継起性（Seriality） ∀x∃y(xRy)

有向性（Directedness） ∀x, y, z((xRy&xRz)⊃ ∃w(yRw&zRw)) ユークリッド性（Euclidean） ∀x, y, z(xRy&xRz ⊃yRz)

空関係（Emptiness） ∀x, y(xRy ⊃ ⊥)

よって表現される性質である．このことから，この規則が，単調性を表現する規則として の働きをすることがわかる．では，次はRに関する規則である．第1章で見たフレーム 条件は，実は次のような一般的な形をしている．幾何学的含意（Geometric Implication） は (Simpson 1994, Negri 2005, Yamasaki and Sano 2016)などで扱われている．

定義 43 (幾何学的含意). 幾何学的含意（Geometric Implication）は一階の述語論理の形 をした以下のような形の文である：

∀⃗x(S1&· · ·&Sm ⊃ ∃⃗y ∨

1⩽j⩽n

(Tj1&· · ·&Tjnj)),

ここでは，⃗x と ⃗y は，一階の述語論理における異なる変項の対からなる有限対（finite taples^{）である．また，}⃗x^と⃗yの両方に出現する変項は存在しないこと，そして，S1, ..., Sm

とT_j1, ..., T_jnj はxRyの形をした原子述語であることを仮定する．最後に，私たちがこ こで用いる二項述語Rを解釈するために，定義17のF = ⟨W, R⟩^からRを用いることに する．

本論で扱うフレーム条件は表4.2のように与えられる^*1．

この形をしたフレーム条件は以下のGRS 図式に沿って規則に書き換えることができ る．この定義 43の幾何学的含意をσ とすると：

*1フレーム条件については表1.2でも与えたが，ここでは，空関係の条件を加え，再掲する．

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

σ :=∀⃗x(S1&· · ·&Sm ⊃ ∃⃗y ∨

1⩽j⩽n

(Tj1&· · ·&Tjn_j)),

ここでは， (Negri 2005, Dyckhoff and Negri 2012)でのように，簡単さのために，常に

⃗

yの長さが1であると仮定されている．このとき，どんな幾何学的含意σ も幾何学的規則 図式（Geometric Rule Scheme, GRS）:

T₁[z₁/y₁], S,Γ⇒∆ · · · T_n[z_n/y_n], S,Γ⇒∆

S,Γ⇒∆ (GRS)

,

と呼ばれる推論規則へと変形できる．ここでは，[z_i/y_i] はy_i へのz_i の代入を表してお り，z1, ..., zn は結論には出現しない．また，S はxRy の形をした原子述語の多重集合 S₁, ..., S_mを表している．同様に，T_jはxRyの形をした原子述語の多重集合T_j1, ..., T_jkj を表している．幾何学的規則図式が次の形∀⃗x(S1&· · ·&Sm ⊃ ⊥)をしているときには，

対応する規則として以下の形をとる：

S,Γ⇒∆ (GRS) .

前提のない形で与えられるこの特別な規則は，前提なしの幾何学的規則図式（zero-premise geometric rule scheme）と呼ばれる．フレーム条件から(GRS)を用いて与えられる規則 は表 4.3のように与えられる．

表4.3 (GRS)の例 (Yamasaki and Sano 2016)

フレーム条件 (GRS)

反射性 xRx,Γ⇒∆ Γ⇒∆ (Ref)

推移性 xRy, yRz, xRz,Γ⇒∆

xRy, yRz,Γ⇒∆ (T ran)

対称性 xRy, yRx,Γ⇒∆

xRy,Γ⇒∆ (Sym)

連結性 xRy, xRz, yRz,Γ⇒∆ xRy, xRz, zRy,Γ⇒∆

xRy, xRz,Γ⇒∆ (Con)

継起性 xRy,Γ⇒∆

Γ⇒∆ (Ser) y is fresh 有向性 xRy, xRz, yRw, zRw,Γ⇒∆

xRy, xRz,Γ⇒∆ (Dir) w is fresh ユークリッド性 xRy, xRz, yRz,Γ⇒∆

xRy, xRz,Γ⇒∆ (Euc)

空関係 xRy,Γ⇒∆(Emp)

第4章 ラベル付きシークエント計算の体系 90 定義 44. 幾何学的規則図式たちの例からなる有限集合 ∗^{を用いて，}G3Fを拡張した体 系を G3F^∗ と書く．また，原子命題の単調性についての規則である (M on)によって，

G3F^∗を拡張したことをG3Fm^∗と書く．G3F(m)^∗を用いて，G3F^∗とG3Fm^∗を表 していることとする．

次にシークエントの構成要素についての用語を導入する．以下で与える，定義 45から 定義 50は，第2章，あるいは第3章で与えられた定義と基本的には同じものであるが，

わかりやすさのため，再掲することとした．従って先に述べたように，以下の議論の流れ はG3Iなどの場合と同様に進む．

定義 45 (文脈，主式). G3F(m)^∗ の推論規則におけるΓと∆は文脈（context）と呼ば れる．G3F(m)^∗の各規則の結論において，文脈に含まれていない論理式（たち）は主式

（principal formula(s)^{）と呼ばれる．}

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

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

そのエンドシークエントがΓ⇒∆であるようなG3F(m)^∗ における導出D^{を持つなら，}

Γ ⇒ ∆はG3F(m)^∗ において導出可能（derivable）である（G3F(m)^∗ ⊢ Γ ⇒∆と書 く）．Γ⇒∆の証明図がせいぜい高さnであることをG3F(m)^∗ ⊢n Γ⇒∆と書く．

もしも，そのことが文脈から明らかな場合には，しばしば“G3F(m)^∗ ⊢Γ⇒∆”という 表現から“G3F(m)^∗”を省略する．

今，G3F(m)^∗では，複合式の同一性が成り立つ．

命題 21 (複合式の同一性, (Yamasaki and Sano 2016, Proposition 1)). 任意の論理式A に対して，G3F(m)^∗ においてx:A,Γ⇒∆, x:Aが導出可能である．

このように与えられるG3F(m)^∗ では，クリプキモデルに対して健全性と完全性が成 り立つ．

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