ジラール埋め込み

各論理体系が持つ命題というのは，第1章でもみたように，そこで扱われる結合子がど のような性質を持つのかによって左右される．ここでは，直観主義論理が線形論理に埋め 込み可能であることについてみる．

直観主義論理と線形論理との間の違いを生み出している要因の一つは，弱化と縮約を認 めるか認めないかの違いである．というのも，縮約や弱化があれば，乗法的・加法的な結 合子は，その同値性を以下のように示すことができるからである：

A ⇒A (Id)

A&B ⇒A (L&) B ⇒B (Id) A&B⇒B (L&) A&B, A&B⇒A⊗B (R⊗)

A&B⇒A⊗B (LC)

A ⇒A (Id)

A, B ⇒A (LW) B⇒B (Id) A, B ⇒B (LW) A, B ⇒A&B (R&) A⊗B⇒A&B (L⊗)

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

表5.2 GLL(Troelstra and Schwichtenberg 2000) (Axioms)

A⇒A (Ax) (Logical Constants)

0,Γ⇒∆ (L0)

Γ⇒∆,⊤ (R⊤)

⊥ ⇒ (L⊥)

⇒1 (R1) (Logical Rules) (i) Logical constants

Γ⇒∆

1,Γ⇒∆ (L1) Γ⇒∆

Γ⇒∆,⊥ (R⊥) (ii) Negation

Γ⇒∆, A

Γ,∼A⇒∆ (L∼) Γ, A⇒∆

Γ⇒∆,∼A (R∼) (iii) Cut

Γ⇒∆, A A,Π⇒Σ Γ,Π⇒∆,Σ (Cut) (iv) Multiplicative (context-free)

A, B,Γ⇒∆

A⊗B,Γ⇒∆ (L⊗) Γ⇒∆, A Π⇒Σ, B

Γ,Π ⇒∆,Σ, A⊗B (R⊗) A,Γ⇒∆ B,Π⇒Σ

APB,Γ,Π⇒∆,Σ (LP) Γ⇒∆, A, B

Γ⇒∆, APB (RP)

Γ⇒∆, A B,Π⇒Σ

A⊸B,Γ,Π⇒∆,Σ (L⊸) A,Γ⇒∆, B

Γ⇒∆, A⊸B (R⊸) (v) Additive (contextual)

A,Γ⇒∆

A&B,Γ⇒∆ (L&1) B,Γ⇒∆

A&B,Γ⇒∆ (L&2) Γ⇒∆, A Γ⇒∆, B Γ⇒∆, A&B (R&) A,Γ⇒∆ B,Γ⇒∆

A⊕B,Γ⇒∆ (L⊕) Γ⇒∆, A

Γ⇒∆, A⊕B (R⊕1) Γ⇒∆, B

Γ⇒∆, A⊕B (R⊕2) Γ⇒∆, A B,Γ⇒∆

Γ, A;B⇒∆ (L;) Γ⇒B,∆

Γ⇒A;B,∆, (R;1) Γ, A⇒∆

Γ⇒A;B,∆ (R;2) (vi) Exponentials

A,Γ⇒∆

!A,Γ⇒∆ (L!) !Γ⇒?∆, A

!Γ⇒?∆,!A (R!) A,!Γ⇒?∆

?A,!Γ⇒?∆ (L?) Γ⇒∆, A Γ⇒∆,?A (R?)

Γ⇒∆

!A,Γ⇒∆ (LW!) Γ⇒∆

Γ⇒∆,?A (RW?) !A,!A,Γ⇒∆

!A,Γ⇒∆ (LC!) Γ⇒∆,?A,?A

Γ⇒∆,?A (RC?) Γ ≡ A1, . . . , Anなら，そのとき!Γ≡!A1, . . . , !An（?の場合も同様である）．

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

A⇒A (Id)

A⇒A, B (RW) B⇒B (Id) B ⇒A, B (RW) A, B ⇒APB (RP) A⊗B ⇒APB (L⊗)

A⇒A (Id)

A ⇒A⊗B (R⊗) B⇒B (Id) B ⇒A⊗B (R⊗) APB ⇒A⊗B, A⊗B (LP)

APB ⇒A⊗B (RC)

そのため，結合子が多い論理体系では，概念の統合が行われていないということであり，

結合子を多く持つ線形論理は直観主義論理よりも繊細な概念分析を行うことができると考 えられるのである．

直観主義論理が線形論理に埋め込み可能であるという結果は，ジラールによってそ の考察が行われた (Girard 1987)．この埋め込みのことをここでは，ジラール埋め込み

（Girard embedding）と呼ぶ．その際に用いられた翻訳は以下：

定義 53 (ジラール翻訳 (·)^∗).

(P)^∗ := P

(⊥)^∗ := 0 (A∧B)^∗ := A^∗&B^∗ (A∨B)^∗ := !A^∗⊕!B^∗ (A⊃B)^∗ := !A^∗⊸B^∗ この翻訳の下で，以下のような埋め込みの結果が得られた．

命題 33 (ジラール埋め込み, (Troelstra 1992, Theorem 5.11)).

Int⊢Γ ⇒Aであることと，LL⊢!Γ^∗ ⇒A^∗であることは同値である．

この結果からわかるのは，上記の翻訳を用いれば直観主義論理を弱い論理であるところの 線形論理を用いて十分に解釈できるということである^*8．このとき，注目すべき点は二つ

*8ただし，様相同伴関係についての際にもそうであったように，翻訳は一つであるとは限らない．翻訳を変 えて埋め込みを行った結果が，それぞれどのような関係にあるのかについては，考察すべき重要な問題で はあるがここでは措く．また，解釈という用語の使い方にも注意が必要である．本論では，「直観主義論 理を線形論理を用いて解釈する」と述べているが，解釈というときには，解釈する側の演算子，ここでは，

線形論理の演算子がより具体的にどのような演算子であるかが明らかでなければならない．しかし，線形 論理の演算子をどのようなもの考えるかは，実は，そう明らかではない．そのため，解釈という用語を用 いるのが適切であるか否かに関しては，慎重な議論を要するが，のちに見るように，ここではひとまず，

直観主義論理の演算子を線形論理の演算子たちを組み合わせて表現できるということを概ね指すと考えて 議論を進める．線形論理の演算子がより具体的に直観主義論理の演算子を解釈しうるのかについては，今 後引き続き検討が必要とされる．

第5章 ベーシックロジックと線形論理 129 ある．一つ目は，原子式の翻訳の仕方についてである．ここでは，直観主義論理の原子式 は，線形論理の原子式へとそのまま埋め込まれる．これは，様相論理S4への埋め込みの 場合とは異なり，直観主義論理と線形論理では，原子式はそのままで構わないということ を表している（ただし，あとで見るようにシークエントレベルでの翻訳を考えた際に前件 にのみ!を付す必要がある．これは，論理式レベルの翻訳とシークエントレベルでの翻訳 では異なる解釈が必要であることを表している）．また，ここでは，連言と選言について は，線形論理の加法的結合子に翻訳されていることから，ここでは直観主義論理の連言，

選言結合子は，線形論理の乗法的な結合子と見るのではなく，加法的な結合子と考えれば 十分であるとみなされているということがわかる．

では，このジラールによって与えられた翻訳以外に直観主義論理を線形論理へと埋め込 む翻訳は考えられないだろうか．以下ではその点について，検討してみよう．