第 4 章 ラベル付きシークエント計算の体系 83
5.3 直観主義論理と線形論理
5.3.2 直観主義論理の線形論理への埋め込み
第5章 ベーシックロジックと線形論理 129 ある．一つ目は，原子式の翻訳の仕方についてである．ここでは，直観主義論理の原子式 は，線形論理の原子式へとそのまま埋め込まれる．これは，様相論理S4への埋め込みの 場合とは異なり，直観主義論理と線形論理では，原子式はそのままで構わないということ を表している（ただし，あとで見るようにシークエントレベルでの翻訳を考えた際に前件 にのみ!を付す必要がある．これは，論理式レベルの翻訳とシークエントレベルでの翻訳 では異なる解釈が必要であることを表している）．また，ここでは，連言と選言について は，線形論理の加法的結合子に翻訳されていることから，ここでは直観主義論理の連言，
選言結合子は，線形論理の乗法的な結合子と見るのではなく，加法的な結合子と考えれば 十分であるとみなされているということがわかる．
では，このジラールによって与えられた翻訳以外に直観主義論理を線形論理へと埋め込 む翻訳は考えられないだろうか．以下ではその点について，検討してみよう．
第5章 ベーシックロジックと線形論理 130 定理 10.
G3I⊢Γ⇒∆ ならば，GLL⊢!Γl ⇒?∆r．
Proof. G3I⊢Γ⇒∆の証明図の高さについての帰納法で示す．
(n= 0)
(Id) このとき，G3Iでは次のような形をしている（Γ≡P,Γ′，∆≡P,∆′）：
P,Γ′ ⇒∆′, P (Id)
GLLの対応する証明図は以下（!Γl≡!P,!Γ′l，?∆r ≡?∆′r,?P）：
P ⇒P (Ax)
!P ⇒P (L!)
!P ⇒?P (R?)
!P,!Γ′l⇒?P (LW!)
!P,!Γ′l ⇒?∆′r,?P (RW?) .
二重線は，(LW!)と(RW?)をそれぞれ必要な回数適用することを表す．
(L⊥) G3Iにおいては次のようになる（Γ≡ ⊥,Γ′）：
⊥,Γ′ ⇒∆ (L⊥) . GLLでの対応する証明図は以下（!Γl ≡ !⊥,!Γ′l）：
⊥ ⇒ (L⊥)
!⊥ ⇒ (L!)
!⊥,!Γ′l ⇒ (LW!)
!⊥,!Γ′l ⇒?∆r (RW?) .
二重線は，(LW!)と(RW?)をそれぞれ必要な回数適用することを表す．
(n >0) G3I⊢Γ ⇒∆で最後に適用された推論規則で場合分けを行う．
(L&) G3Iでの証明図は次のような形をしている（Γ≡A&B,Γ′）： ....
A, B,Γ′ ⇒∆
A&B,Γ′ ⇒∆ (L&) .
第5章 ベーシックロジックと線形論理 131 まず，帰納法の仮定を適用し，GLL で以下のような証明図を手にできる
（!Γl≡!(!Al⊗!Bl),!Γ′l）：
....
!Al,!Bl,!Γ′l⇒?∆r
!Al⊗!Bl,!Γ′l⇒?∆r (L⊗)
!(!Al⊗!Bl),!Γ′l⇒?∆r (L!) .
(R&) G3Iの証明図は次のような形をしている（∆≡∆′, A&B）：
....
Γ⇒∆′, A
....
Γ⇒∆′, B
Γ⇒∆′, A&B (R&) .
まず，この前提に帰納法の仮定を適用し，GLLでの対応する次のような証明 図を手にできる（?∆r ≡?∆′r,?(?Ar⊗?Br)）：
....
!Γl⇒?∆′r,?Ar
....
!Γl ⇒?∆′r,?Br
!Γl,!Γl⇒?∆′r,?∆′r,?Ar⊗?Br (R⊗)
!Γl,!Γl ⇒?∆′r,?∆′r,?(?Ar⊗?Br) (R?)
!Γl⇒?∆′r,?∆′r,?(?Ar⊗?Br) (LC!)
!Γl ⇒?∆′r,?(?Ar⊗?Br) (RC?) .
二重線は，(LC!)と(RC?)をそれぞれ必要な回数適用することを表す．
(L∨) G3Iでは次のような形をしている（Γ≡A∨B,Γ′）： ....
A,Γ′ ⇒∆
....
B,Γ′ ⇒∆ A∨B,Γ′ ⇒∆ (L∨)
まず帰納法の仮定を適用し，GLLで以下のような証明図を手にできる（!Γl ≡
!(!AlP!Bl),!Γ′l）：
第5章 ベーシックロジックと線形論理 132
....
!Al,!Γ′l⇒?∆r
....
!Bl,!Γ′l⇒?∆r
!AlP!Bl,!Γ′l,!Γ′l⇒?∆r,?∆r (LP)
!(!AlP!Bl),!Γ′l,!Γ′l ⇒?∆r,?∆r (L!)
!(!AlP!Bl),!Γ′l⇒?∆r,∆r (LC!)
!(!AlP!Bl),!Γ′l⇒?∆r (RC?) .
二重線は，(LC!)と(RC?)をそれぞれ必要な回数適用することを表す．
(R∨) G3Iの証明図は次のような形をしている（∆≡∆′, A∨B）：
....
Γ⇒∆′, A, B
Γ⇒∆′, A∨B (R∨) .
まず，帰納法の仮定を適用し，GLL で以下の証明図を手にできる（?∆r ≡
?∆′r,?(?ArP?Br)）：
....
!Γl ⇒?∆′r,?Ar,?Br
!Γl ⇒?∆′r,?ArP?Br (RP)
!Γl⇒?∆′r,?(?ArP?Br) (R?) .
(L⊃) このとき，G3Iでは次のような形をしている（Γ≡A⊃B,Γ′）： ....
A⊃B,Γ′ ⇒∆, A
....
B,Γ′ ⇒∆ A⊃B,Γ′ ⇒∆ (L⊃)
.
帰納法の仮定を適用し，GLL で以下のような証明図を手にできる（!Γl ≡
!(?Ar⊸!Bl)）：
....
!(?Ar⊸!Bl),!Γ′l⇒?∆r,?Ar
....
!Bl,!Γ′l ⇒?∆r
!(?Ar⊸!Bl),!Γ′l,!Γ′l,?Ar⊸!Bl⇒?∆r,?∆r (L⊸)
!(?Ar⊸!Bl),!Γ′l,!Γ′l,!(?Ar⊸!Bl)⇒?∆r,?∆r (L!)
!(?Ar⊸!Bl),!Γ′l ⇒?∆r,?∆r (LC!)
!(?Ar⊸!Bl),!Γ′l⇒?∆r (RC?)
.
第5章 ベーシックロジックと線形論理 133 二重線は，(LC!)と(RC?)をそれぞれ必要な回数適用することを表す．
(R⊃) G3Iでは次のような形をしている（∆≡∆′, A⊃B）： ....
Γ, A ⇒B
Γ⇒∆′, A⊃B (R⊃) .
帰納法の仮定を適用し，GLL で次のような証明図を手にできる（?∆r ≡
?∆′r,?(!Al⊸?Br)）：
....
!Γl,!Al⇒?Br
!Γl ⇒!Al⊸?Br (R⊸)
!Γl⇒?(!Al⊸?Br) (R?)
!Γl ⇒?∆′r,?(!Al⊸?Br) (RW?) . 二重線は，(RW?)を必要な回数適用することを表している．
この補題の証明から次のことがわかる：
• GLL側では，(RW?)を使うのは(Id)と(L⊥)と(R⊃)の場合のみ．
• 線形論理の翻訳先の結合子は，乗法的なものを用いても良い．ただし，!と?につい ての縮約の規則が必要となる．
一点目から，直観主義論理のシークエントが持つべき特徴を再考しようとした際，シー クエントのどの部分が本当に後件一つでなければならないのかということがわかる．一般 的に言われるLJの一番の特徴はシークエントの後件の論理式の出現をたかだか一つに制 限することである．ここで用いた後件複数のG3Iの体系はLJの制限を可能な限り緩め，
拡張した体系である．この体系を用いて，弱化や縮約に対してもより強い制限を課す，線 形論理への埋め込みを考え，線形論理のどこに弱化が適用されたのかを考えることによっ てLJのシークエントのどこが本当に後件一つでなければならないのかを明らかにするこ とができたと考えられる．
続く二点目についてであるが，この翻訳を用いても線形論理への埋め込みが可能である ということから，ベースとなる各結合子は，乗法的なもので十分ということがわかる．証 明図を見ると，線形論理側では，乗法的な結合子は，!と?の弱化や縮約と協力することに
第5章 ベーシックロジックと線形論理 134 よって，加法的な形で与えられている直観主義論理の結合子を解釈する証明図を与えるこ とが可能となっていることがわかる．結合子が持つ性質を明らかにしようとする際には，
よりプリミティブな性質を提示できる方が好ましいと考えられるので，解釈に用いる線形 論理側での結合子は乗法的な性質を持つ形でその翻訳を与えておく方がここでの趣旨に則 した翻訳であると考えられる．