結合子の推論規則についての正当化

2.1 節の冒頭で見た推論の二つの基本原則を思い出そう．ここでは，説明のため記号化 も交えた形で与える．それは次のようなものであった．

(i) ある命題Aを仮定したら，その命題自身Aを結論して良い．

(ii) ^ある命題A^{から，ある命題}B^{を結論できるとき（}A⇒B^{），この命題}A^が実際に 帰結しているなら（⇒A），この帰結関係（⇒A）は，先の帰結関係（A ⇒B）と 組み合わさって，ある命題Bが帰結する（⇒B）．

この二つの基本原則のうち，(ii)は(i)とは異なり，帰結関係の構造が，入れ子になっ ていることに注意しなければならない．ここでは例えば，A ⇒ B^の中にはA^とB^の間 に論理式の間の帰結関係が存在する．次に，⇒AとA⇒Bから，⇒Bを導き出す際に も，シークエントの間の帰結関係が存在する．つまり，一つの推論（帰結関係）を一つの 対象とみなし，それらの間にも，推論を行う（帰結関係が存在する）ことができるという ことである．ここでは，このような推論関係を「推論の構造に関係する推論」と呼ぶこと にし，「メタレベル」，あるいは，「構造レベル」の推論と表現する．一方，メタレベルの 推論ではないものを単に「推論」と呼び，「対象レベル」，あるいは，「命題レベル」の推論 と表現する．

ベーシックロジックでは，結合子をこのメタレベルの推論の構造を反映させたものと見 なす．ベーシックロジックの目的の一つは，様々な論理たちの宇宙の中に，一つの構造を 見出すこと（ (Sambin et al. 2000, p.979)）．また，定義方程式（definitional equation） を解くという仕方で，各結合子の推論規則を定めるという方法をとると，推論規則をメタ の構造を推論規則の中に反映させることができるという形で正当化することをもまた目的 としている．

*2ベーシックロジックについては，(大西2012)でもその詳しい説明が与えられている．

第5章 ベーシックロジックと線形論理 113 ベーシックロジックは，三つの特徴的な性質を持つ：(i) reflection（反映）；(ii) symmetry

（対称性）；(iii) visibility（可視性）．(iii)はシークエントが持つ性質のことを指し，シー クエントの前件（後件）に出現する論理式がたかだか一つであるときに，シークエントの 前件（後件）は可視性を持つと言う．また，(i)から（少なくとも）(ii)の条件が自然と帰 結することがわかるので，ここでは，(i)について少し詳しく見て行こう．ここでの反映

とは，(大西 2009, p.142)の中でまとめられているように，以下のようなテーゼが意図さ

れていると考えるのがよいだろう：

「論理定項とはシークエント・レベルの構造に対する，命題レベルでの反映である」

ここでのシークエント・レベルとは，先ほど述べた，メタレベルのことと考えてよい．結 合子というのはメタレベルでの構造を反映した形で与えられているものであるということ を表しており（これは反映原理 (principle of reflection)と言われる），メタレベルの構造 を反映した形で与えられる結合子を選択するのがよいということが意図されている．メタ レベルの構造を表現する語は，「yields（与える）」，「and（と）」の二つのみであると考えて おき， (Sambin et al. 2000)では，この二つの語が「link」と呼ばれる．このとき，ベー シックロジックで扱われる各結合子（⊗,P,&,⊕,→,←）の推論規則は，この二つのlinkが あれば与えることができる．

ではここで，具体的な議論に入る前に，まず簡単に記号法と用語法を定める．A, B, C, . . . は論理式を表現する．A1 and . . . and An の略記としてA1, . . . , Anを用いる．シークエ ントの定義は Defintion 22と同じでよい．また，ここでは，シークエントは「Γ yields

∆」によって表現されるのであるが，「Γ⊢∆」と書かれ，「∆はΓの帰結である」という ことを表現していると考えてよい．また，Γ⊢∆において，⊢をこのシークエントの主結 合（main connective）と呼ぶこととする．論理記号で表現されたとき，“⊢”は「yields」 の，“,”は「and」の，それぞれ省略とみなされていることがわかる．ここでの推論規則 は，例えば

Γ^′ ⊢∆^′ Γ⊢∆ (r)

のように書き，「Γ^′ ⊢ ∆^′ から Γ ⊢ ∆ へと移行ができること（we can move from the assertion Γ^′ ⊢ ∆^′ to the assertion Γ ⊢ ∆. (Sambin et al. 2000, p.984)）」を表現して いる．このとき，この一つのシークエントから異なるシークエントへの移動には，これま

第5章 ベーシックロジックと線形論理 114

でのyieldsによって表現されていたのとは異なるレベルの帰結関係が用いられているこ

とがわかる．つまり，推論規則の中には，本質的に，推論についてのメタ概念が用いられ ているということである．これが，先ほど指摘した，(ii)の原則の中に潜んでいた帰結関 係が持つ入れ子構造の正体である．

linkの一つであるandが最も外側の結合である場合には，「(Γ^′ ⊢ ∆^′) and (Γ^′′ ⊢∆^′′)」 が「Γ^′ ⊢∆^′ とΓ^′′ ⊢∆^′′が同時に成り立っている」を表現するが，andがyieldsの内部に 入ってしまった時は，そうではなくなる．つまり，A and B ⊢ ∆のように，andが論理 式の内部に入り込んでしまったときには，「A and B ⊢∆」は「A⊢∆ and B ⊢∆」と同 値ではなくなる．このことは，⊢^{の左側に，}andが入ったときにも言える．その場合は，

「Γ⊢ A and Γ ⊢B」と「Γ⊢ A and B」が同値ではなくなる．したがって，最も外側の 結合にならないandは，一般的に「と」に期待されるような推論的性質は持たないという ことである．そのため，ここまで見てきたシークエント計算の体系では，シークエントの 後件では「,」は「または」と解釈されたが，ベーシックロジックでは「かつ」と考えてお けば十分であるということがわかる．

一方，yieldsが最も外側にあるときには，メタのメタの帰結関係を表し，「(Γ^′ ⊢∆^′) ⊢ (Γ⊢∆)」は「Γ^′ ⊢∆^′からΓ⊢∆が帰結する」が表現するものと同じである．このとき，

この二つの表現の同値性から，シークエントの二つの合成（composition）を与えること ができる．（表記ϕ(Γ/A)はϕ中のAをΓで置き換えるということを表す）：

Γ⊢A Γ^′ ⊢∆

Γ^′(Γ/A)⊢∆ (LCut) Γ⊢∆^′ A ⊢∆

Γ⊢∆^′(∆/A) (RCut)

これはいわゆるカット規則である．このとき，シークエントの同一性と合成が，それぞ れ，推論の基本原則(i)，(ii)で表現されたものにあたると考えてよい．

ここでまず，一般的に，定義方程式とは何か，定義方程式を解くとはどういうことであ るのかということを確認する．

新しい結合子◦ を与えたいとすると，その結合子が満たすべき同値性を参考にして，

その欲しい結合子を定める．このとき，その同値性のことを「定義方程式 (definitional

equation)」と呼ぶ．それは例えば，以下のような形で与えられる：

任意の∆に対して，(A◦B ⊢∆) ⇔ ((A and B) ⊢ ∆)

第5章 ベーシックロジックと線形論理 115 ここでの⇔^は，⊢が両方向に成り立っているということを表現しているが，この⇔^は，

メタのメタの構造に関係する帰結関係を表現している．また，この両辺は，左辺が被定 義項，右辺が定義項である．このとき，右辺から左辺への方向から，次の規則が自然に生 じる：

A and B ⊢∆ A◦B⊢∆ .

この方向の規則は，一般に形成（formation）の規則と言われる．一方，この逆向きは，定 義されるべき◦がすでに前提中に出現しているので，そのままでは，◦^{についての明示的} な情報を与えてはくれなさそうである：

A◦B⊢∆ A and B ⊢∆ .

そういうわけで，この◦ を前提ではなく結論中に出現するように変形しなければならな い．以下に見るような一定の操作を行えば，必要な規則が手にできる．そのため，まず∆ をA◦Bとすることで，

A◦B ⊢A◦B A and B⊢A◦B

となる．続いて，A◦B ⊢A◦Bは同一性を表す推論の前提（つまり，公理）であるため消 し，A and B⊢A◦Bを手にする．このとき，andは「,」で略記されるので，A, B⊢A◦B となる．そして，Γ⊢ AとΓ^′ ⊢Bが成立していると仮定して，次のように変形を行うこ とができる：

Γ^′ ⊢B

Γ⊢A A, B ⊢A◦B

Γ, B⊢A◦B (LCut) Γ,Γ^′ ⊢A◦B (LCut)

.

さらに，A, B ⊢ A◦Bは公理とみることができるのでないものと考えてよく，以下の規 則を手にできる：

Γ ⊢A Γ^′ ⊢B Γ,Γ^′ ⊢A◦B .

この規則は，先の定義方程式の，左辺から右辺の方向から導出可能であることがわかる．

そのため，この方向の変形後の規則は「明示的反映（explicit reflection）」規則と呼ばれ

第5章 ベーシックロジックと線形論理 116 る．このような二つの規則（形成規則と明示的反映規則）を与えることによって，◦^の振 る舞いを定義することができる．ここで見たような仕方で，各結合子は，定義方程式を解 くという形で，その推論規則を定めることができる．このとき，ここまで見てきた◦^は結 合子 ⊗の説明となっている．では以下で，具体的に各結合子（⊗^{も再度見るが）につい} て見てみよう．

二つのlink，andとyieldsは，そのスコープの違いによって，その性質が区別され，対 象言語の中でここで問題にしている六つの結合子に反映される．andが連言・選言に反映

され，yieldsが含意に反映される．また，その反映のされ方は，各linkがシークエントの

どの位置に出現するのか，どちらのlinkが最も外側の結合になっているのかで変わってく る．まず，⊢によって表現されているシークエントの主結合としてのyieldsが最も外側の 結合になる場合を考える．このとき，もう一つのlinkであるandが主結合のyieldsの左 右どちらに出現するかを考察することで，andの振る舞いを調べることができる．まず，

andがシークエントの主結合の左側に出現している場合を見る．その定義方程式は以下：

任意の∆に対して，(A⊗B⊢∆) ⇔ ((A, B)⊢∆)

このとき，⊢によって表現されているシークエントの主結合としてのyieldsの左側に出 てくるandの性質を対象レベルの論理結合子⊗が反映しているということになる．この 定義方程式を解くことによって⊗の二つの規則が与えられる（⊗^{の形成規則を「}(⊗-F)」 と，⊗^{の隠伏的規則を「}(I⊗-F)^{」と，それぞれ書く）：}

A, B ⊢∆

A⊗B ⊢∆ (⊗-F) A⊗B ⊢∆

A, B ⊢∆ (I⊗-R)

これら二つの規則は，結合子⊗^をyieldsの左側のコンマ，つまり，andの反映として定 める．このとき，形成規則に関しては，このままでも，結合子の意味を与える規則になっ ている．しかし，先ほども見たように，反映規則の方はそうではない．そこで，先ほど見 たのと同様の変形を行う．まず，規則の∆をA⊗Bと見なし，

A⊗B ⊢A⊗B A, B ⊢A⊗B

を手にする．A⊗B ⊢A⊗B は公理なので消し，(I⊗-R)と同値な，A, B ⊢ A⊗Bを手 にする．このとき，（AとB はそれぞれが，Γ ⊢ A, Γ^′ ⊢ Bから導き出されると考えて）

次のような推論を行える：