第 3 章 証明構造 22
3.3.2 帰納的証明構造に関する 概念
論理式に 対し て 定義や補題と し て 与え ら れて いる も のを 、 こ の帰納的証明構造 で用いる ために節点に対し て 定義する 。
定義(部分節点).
xA ∈Vαの部分節点sub(x)は以下のよ う に定義さ れる 。
• sub(xpL)= sub(xpR)={x}
• sub(x0L)= sub(x0R)=∅
• sub(x(B⊸C)L)= sub(x(B⊸C)R)= sub(y)∪sub(z)∪ {x}
ただし 、 {y,x},{z,x} ∈ Eαである 。
定義(狭義の擬正節点(pseudo strictly positive vertex)).
xA ∈Vαの狭義の擬正節点sub++(x)は以下のよ う に定義さ れる 。
• sub++(xpL)= sub++(xpR)={x}
• sub++(x0L)= sub++(x0R)=∅
• sub++(x(B⊸C)L)= sub++(yCL)∪ {x}
• sub++(x(B⊸C)R)= sub++(yCR)∪ {x}
ただし 、 {y,x} ∈ Eαである 。
定義(狭義の擬負節点(pseudo strictly negative vertex)). xA ∈ Vαの狭義の擬負節点 sub−−(x)は以下のよ う に定義さ れる 。
• sub−−(xpL)= sub−−(xpR)={x}
• sub−−(x0L)= sub−−(x0R)=∅
• sub−−(x(B⊸C)L)= sub−−(yBL)∪ {x}
• sub−−(x(B⊸C)R)= sub−−(yBR)∪ {x}
ただし 、 {y,x} ∈ Eαである 。 定義(退去節点と 進入節点).
x∈Vαの退去節点LE(x)と 進入節点EN(x)は以下のよ う に定義さ れる 。
• LE(x)= max({y| x∈sub++(y)})
• EN(x) =min({y|LE(x) ∈sub−−(y)})
こ こ でこ れま での概念に対し て 例を 挙げる 。
pL pR qL qR rL rR
ax ax ax
⊸L
(p⊸q)L
⊸L
(q⊸r)L
⊸R
((p⊸q)⊸r)R sub++(((p⊸q)⊸r)R)= {((p⊸q)⊸r)R,rR}
sub−−(((p⊸q)⊸r)R)= {((p⊸q)⊸r)R,(p⊸ q)L,pR} LE(rR)= ((p⊸q)⊸r)R
EN(rR)= ((p⊸q)⊸ r)R
3.3.3 可逆性
こ こ では、 帰納的証明構造に関する 可逆性を 示す。 +除去の補題と 類似し た補題 である 。
補題(可逆性).
• R0に関する 可逆性
T N(α) = {ΓL,∆R,x0R}である αが帰納的証明構造な ら ば、 T N(α′) = {ΓL,∆R} である 帰納的証明構造α′が存在する 。
• R⊸に関する 可逆性
T N(α)={ΓL,∆R,z(A⊸B)R}であるαが帰納的証明構造なら ば、T N(α′)= {ΓL,∆R,xAL,yBR} である 帰納的証明構造α′が存在する 。 ただし 、 {x,z},{y,z} ∈Eαである 。
証明(R0に関する 可逆性).
帰納的証明構造の構成に関する 帰納法で示す。
基底段階
• 公理ま たはL0規則で導出さ れたと き こ れら の場合はx0Rを 含ま な い。
帰納段階
• 最後にR0規則で導出さ れたと き
帰納的証明構造βから R0規則によ っ て αが導出さ れたと する 。
– 最後の規則によ っ て x0Rが導出さ れたと き
帰納的証明構造の定義よ り 、 βは帰納的証明構造であ り 、 求める α′で ある 。
– 最後の規則によ っ て x0R以外が導出さ れたと き
βに帰納法の仮定し て 、 β′が取れる 。 よ っ て 、 β′にR0規則を 適用する こ と で、 求める 帰納的証明構造α′が存在する こ と が分かる 。
• 最後にL⊸規則で導出さ れたと き
帰納的証明構造βと γから L⊸規則によ っ てαが導出さ れたと する 。 x0R ∈Vβ と し 、 βに帰納法の仮定を 適用し たも のを β′と する 。 こ のと き 、 以下のよ う に αを 再構成でき る 。
β′ γ α′ L⊸
α R0
し たがって、 求める 帰納的証明構造α′が存在する こ と が分かる 。 ま た、 x∈Vγ に対し て も 同様の議論ができ る 。
• 最後にR⊸規則で導出さ れたと き
帰納的証明構造βから R⊸規則によ っ て αが導出さ れたと する 。 βに帰納法 の仮定を 適用し たも のを β′と する 。 こ のと き 、 以下のよ う に αを 再構成で き る 。
β′ α′ R⊸
α R0
し たがっ て 、 求める 帰納的証明構造α′が存在する こ と が分かる 。
証明(R⊸に関する 可逆性).
帰納的証明構造の構成に関する 帰納法で示す。
基底段階
• 公理ま たはL0によ っ て 導出さ れたと き こ れら の場合はz(A⊸B)Rを 含ま な い。
帰納段階
• 最後にR0よ っ て 導出さ れたと き
帰納的証明構造βから R0規則に よ っ て αが導出さ れたと する 。 βに 帰納法
の仮定を 適用し たも のを β′と する 。 こ のと き 、 以下のよ う に αを 再構成で き る 。
β′ α′ R0
α R⊸
し たがっ て 、 求める 帰納的証明構造α′が存在する こ と が分かる 。
• 最後にL⊸よ っ て 導出さ れたと き
帰納的証明構造βと γから L ⊸規則によってαが導出さ れたと する 。 z(A⊸B)R ∈ Vβと し 、 βに帰納法の仮定を 適用し たも のを β′と する 。 こ のと き 、 以下のよ う にαを 再構成でき る 。
β′ γ α′ L⊸
α R⊸
し たがっ て 、 求める 帰納的証明構造α′が存在する こ と が分かる 。 ま た、 z∈γ に対し て も 同様の議論ができ る 。
• 最後にR⊸よ っ て 導出さ れたと き
帰納的証明構造βから R⊸規則によ っ て αが導出さ れたと する 。 – 最後の規則によ っ てz(A⊸B)Rが導出さ れたと き
帰納的証明構造の定義よ り 、 βは帰納的証明構造であり 、 求める α′が存 在する 。
– 最後の規則によ っ てz(A⊸B)R以外が導出さ れたと き
βに 帰納法の仮定し て 、 β′が取れる 。 よ っ て 、 β′に R ⊸規則を する こ と で、 求める 帰納的証明構造α′が存在する こ と が分かる 。
第 4 章 線形論理における 古典論理と 直観主義論理の関係
4.1 ⊸ 結合子だけから なる 線形論理での関係
初めに、 ⊸の結合子だけ を 持つ線形論理について 考え る 。 つま り 、 シーク エン ト 計算は以下の公理と 規則だけ から な る 。
p⇒ p Ax Γ,A⇒∆ Γ′,B⇒ ∆′
Γ,Γ′,A⊸B⇒∆,∆′ L⊸ Γ,A⇒B,∆ Γ⇒A⊸ B,∆ R⊸
こ の線形論理でΓ⇒∆が証明可能である と き 、 MILL ⊢Γ⇒∆と する 。 こ のと き 、 以下の定理が成り 立つ。
定理. 以下の２ 条件は同値である 。 1. MICLL⊢Γ⇒ A
2. MIILL⊢Γ⇒ A
こ の証明には以下の補題が必要である 。 補題. MICLL 0Γ⇒
証明. MICLLの構成に関する 帰納法で示す。
基底段階
• 公理
こ の補題は成り 立つ。
帰納段階
• 最後にL⊸規則で導出さ れたと き
MICLL⊢Γ⇒な ら ば以下の場合が考え ら れる 。 Γ1 ⇒B Γ2,C ⇒
Γ1,Γ2,B⊸C ⇒ L⊸
し かし 、 帰納法の仮定よ り MICLL0Γ′,C ⇒である 。 し たがっ て 、 MICLL 0 Γ⇒が成立する 。
• 最後にR⊸規則で導出さ れたと き 明ら かに MICLL 0Γ⇒である 。
こ の補題を 用いて 先ほど の定理を 証明する 。
証明.
• 1→2
MICLLの構成に関する 帰納法で示す。
基底段階
– MICLL ⊢ p⇒ pのと き
定義から MIILL⊢ p⇒ pである 。 帰納段階
– 最後にL⊸規則で導出さ れたと き
MICLL ⊢Γ1,Γ2,B⊸C⇒ Aな ら ば以下の場合が考え ら れる 。 Γ1 ⇒ B Γ2,C ⇒ A
Γ1,Γ2,B⊸C ⇒A L⊸ Γ1 ⇒ B,A Γ2,C⇒ Γ1,Γ2,B⊸C⇒ A L⊸ 先ほどの補題よ り 、 右側の場合は起こ ら ない。 し たがって、 左側の場合の みを 考える 。 帰納法の仮定よ り 、 MIILL⊢ Γ1⇒ BかつMIILL⊢ Γ2⇒ A である 。 よ っ て 、 MIILL ⊢Γ1,Γ2,B⊸C⇒ Aである 。
– 最後にR⊸規則で導出さ れたと き
MICLL ⊢Γ⇒ B⊸Cな ら ば、 以下の証明図が考え ら れる 。 Γ,B⇒C
Γ⇒B⊸C R⊸
帰納法の仮定よ り MIILL ⊢ Γ,B ⇒ Cな ので、 MIILL ⊢ Γ ⇒ B⊸ Cで ある 。
• 2→1
シーク エン ト 計算の定義から 自明である 。
4.2 MIZLL に関する 関係
次に、 先ほど の論理に定数0を 追加し た線形論理について 考える 。 つま り 、 シー ク エン ト 計算は以下の公理と 規則だけ から な る 。
p⇒ p Ax 0⇒ p L0 Γ⇒ ∆ Γ⇒∆,0 R0 Γ,A⇒ ∆ Γ′,B⇒∆′
Γ,Γ′,A⊸ B⇒∆,∆′ L⊸ Γ,A⇒ B,∆
Γ⇒ A⊸ B,∆ R⊸
先ほど の論理では古典的な論理と 直観主義的な論理は証明能力が同じ であっ たが、
定数0を 加え る こ と で古典的な論理の方が多く の論理式を 証明でき る よ う になる 。
先行研究[5, 6]では、 終式だけ を 見て DNEやそ れに 代わる 集合を 定めて いた。
し かし 、 線形論理では弱化規則と 縮約規則が認めら れて いな いので、 同様に 考え る のは難し い。 し たがっ て 、 終式だけでなく 証明図を 解析し て DNEを 定める 。 公 理と し て 現れた⇒の右側のpが⇒の左側に移る ま での証明図の挙動を 調べる 。 つ ま り 、 以下のよ う な 証明図の点の部分に着目する 。
p⇒ p Ax ...
Γ′ ⇒ P,∆′ Γ′,Q⇒ ∆′ Γ,Γ′,P⊸Q⇒ ∆,∆′
4.2.1 帰納的証明構造を 用いたア プローチ
シーク エン ト 計算の証明図ではな く 、 前章で定義し た帰納的証明構造を 用いて 解析する 。 つま り 、 IPScと IPSiについて 解析する 。 帰納的証明構造の利点と し て 以下の２ つ挙げら れる 。
１ つ目は、 グラ フ 的な 特徴付け ができ る こ と である 。 MIZCLL ⊢∼∼ p⇒ pに対応 する 帰納的証明構造は以下である 。
pL pR 0R 0L
ax
⊸R
(∼ p)R
⊸L
(∼∼ p)L
こ のよ う に 、 論理式間の関係がつな がり で分かる 。 こ のつな がり に 関する 特徴付 け を 試みる 。
２ つ目は、 規則の適用順序だけ の違いである も のの区別を し な く て 良いこ と で ある 。 例と し て 、 ２ つの証明図を 挙げら る 。
⇒ A B,C ⇒ D A⊸ B,C ⇒D L⊸
A⊸ B⇒C ⊸D R⊸ ⇒ A
B,C ⇒D
B⇒C ⊸D R⊸ A⊸ B⇒C⊸ D L⊸
見て 分かる よ う に、 こ れら の違いはL⊸規則と R⊸規則の適用順序の違いだけで ある 。 そし て 、 こ れら ２ つの証明図に対する 帰納的証明構造は以下のよ う になる 。
AR BL CL DR
⊸L
(A⊸ B)L
⊸R
(C⊸ D)R
規則の適用順序だけ の違いを 無く すこ と で、 解析すべき 証明図の数を 減ら すこ と ができ る 。
こ れら ２ つの理由から 、 シーク エン ト 計算ではな く 、 帰納的証明構造を 用いる 。 ま ず、 よ く 知ら れた定理を 帰納的証明構造の形で書き 直す。 今ま では、 T NRが 高々 １ つのIPScに対し て、 それに対応する IPSiが存在する こ と を 示し た。 し かし 、 線形論理では直接証明する こ と がき な い。 そのため、 T NRに制限を 加え な いも の に対し て 示す。
定理. T N(α) = ΓL∪∆Rである IPScαが存在する な ら ば、 T N(αi)= ΓL∪(∼ ∆′)L∪ {yAR} ∪DNEαである IPSiαiが存在する 。
ただし 、 ∆R = ∆′R∪ {yAR}かつ DNE ={x(∼∼p⊸p)L|(x2,pR)∈ Lα,x2 <∆′R}である 。 こ こ で、 x27−→ x<Vαは単射である 。
証明. IPScの構成に関する 帰納法で示す。
基底段階
• 公理で導出さ れたと き
T N(α)={x1pL,x2pR}である IPScαが存在し たと する 。 こ のと き 、 ２ つのIPSiαi
の存在を 示す。
1. T N(αi)={x1pL,x2pR,x(∼∼p⊸p)L}の存在 以下のIPSiが存在する 。
pL pR pL pR 0L
0R
ax ax
⊸L
(∼ p)L
⊸R
(∼∼ p)R
⊸L
(∼∼ p⊸ p)L 2. T N(αi)={x1pL,z2(∼p)L}の存在
以下のIPSiが存在する 。
pL pR 0L
ax
⊸L
(∼ p)L
• L0規則で導出さ れたと き
T N(α) = {x10L}である IPScαが存在し たと する 。 こ のと き 、 T N(αi) = {x10L} である IPSiαiの存在を 示す。 こ れはIPSiの定義よ り 明ら かに存在する 。 帰納段階
• 最後にR0規則で導出さ れたと き
T N(α′) = ΓL ∪∆R ∪ {yAAR}であ る IPSc α′に R0規則を 適用し て 、 T N(α) = ΓL∪∆R∪ {yAAR,y00R}であるIPScαを 構成し たと する 。 こ のと き 、 ３ つのIPSi の存在を 示す。
1. T N(αi)= ΓL∪(∼∆)L∪ {yAAR,z0(∼0)L} ∪DNEαである IPSiαiの存在 α′に R⊸に関する 可逆性を 適用し て 、 T N(β)= ΓL∪ΓAL∪∆R∪ {yaaR}で ある IPScβが取れる 。 こ れに帰納法の仮定を 適用し て 、 T N(βi)= ΓL∪ ΓAL∪(∼∆)L∪ {za(∼a)L} ∪DNEβであるIPScβiが取れる 。 よ っ て 、 以下の 手順でIPSiαi′が取れる 。
βi
βi1
R0 ({x0},∅,{(x0,0L)})
βi2 L⊸ ({xa1,xa2},{(xa1,xa2)},{(xa1,aL),(xa2,aR)})
βi3 L⊸
... αi′
T N(βi1)= ΓL∪ΓAL∪(∼∆)L∪ {za(∼a)L,y00R} ∪DNEβ T N(βi2)= ΓL∪ΓAL∪(∼∆)L∪ {za(∼a)L,z0(∼0)L} ∪DNEβ
T N(βi3)= ΓL∪ΓAL∪(∼∆)L∪ {ya′aR,z0(∼0)L} ∪DNEβ∪ {x(∼∼a⊸a)L} T N(αi′)= ΓL(∼∆)L ∪ {yAAR,z0(∼0)L} ∪DNEβ∪ {x(∼∼a⊸a)L}
最後に、 DNEα = DNEβ∪ {x(∼∼a⊸a)L}な ので、 αi = αi′である 。 2. T N(αi)= ΓL∪(∼∆)L∪ {zA(∼A)L,y00R} ∪DNEαである IPSiαiの存在
α′に帰納法の仮定を 適用し て 、 T N(α′i)= ΓL∪ΓAL∪(∼ ∆)L∪ {zA(∼A)L} ∪ DNEα′ であ る IPSc α′i が取れる 。 こ れに R0規則を 適用し て 、 求める IPSiαiが取れる 。
3. T N(αi)= ΓL∪(∼∆)L,{zA(∼A)L,z0(∼0)L} ∪DNEαである IPSiαiの存在 (2)よ り 、 T N(α′i)= ΓL∪(∼∆)L,{zA(∼A)L,y00R} ∪DNEα′である IPSiα′iが 取れる 。 こ れと T N(βi)= {x10L}である IPSiβiに対し て 、 L ⊸規則を 適 用する こ と で求めるIPSiαiが取れる 。
• 最後にL⊸規則で導出さ れたと き
T N(α1) = ΓL ∪∆R ∪ {yA1AR,x1BR}であ る IPSc α1と 、 T N(α2) = Γ′L ∪∆′R ∪ {yA2A′R,x2CL}である IPScα2に L⊸規則を 適用し て 、 T N(α) = ΓL∪Γ′L∪∆R∪
∆′R∪ {yA1AR,yA2A′R,x3(B⊸C)L}である IPScαを 構成し たと する 。 こ のと き 、 ３ つのIPSiの存在を 示す。
1. T N(αi)= ΓL ∪Γ′L ∪(∼ ∆)L∪(∼ ∆′)L∪ {yA1AR,zA2(∼A′)L,x3(B⊸C)L} ∪DNEα
である IPSiαiの存在
α1 に R ⊸ に 関する 可逆性を 適用し て 、 T N(α1′) = ΓL ∪ ΓAL ∪ ∆R ∪ {yaaR,x1BR}であ る IPSc α1′が取れる 。 α1′ に 帰納法の仮定を 適用し て 、 T N(βi) = ΓL ∪ ΓAL ∪ (∼ ∆)L ∪ {za(∼a)L,x1BR} ∪ DNEα1′ であ る IPSi βi が取れる 。 同様に α2 に 帰納法の仮定を 適用し て 、 T N(γi) = Γ′L ∪ (∼
∆′)L∪ {zA2(∼A′)L,x2CL} ∪DNEα2 である IPSiγiが取れる 。 し たがっ て 、 以 下のよ う にIPSiαi′が構成でき る 。
βi γi
αi′′ L⊸ ...
αi′
T N(αi′′)= ΓL∪ΓAL∪Γ′L∪(∼ ∆)L∪(∼ ∆′)L∪ {za(∼a)L,zA2(∼A′)L,x3(B⊸C)L}
∪DNEα1′∪DNEα2 T N(αi′
)= ΓL∪Γ′L∪(∼ ∆)L∪(∼∆′)L∪ {yA1AR,zA2(∼A′)L,x3(B⊸C)L}
∪DNEα1′∪DNEα2 ∪ {x(∼∼a⊸a)L}
最後に、 DNEα =DNEα1′∪DNEα2∪ {x(∼∼a⊸a)L}なので、 αi =αi′である 。 2. T N(αi)= ΓL∪Γ′L∪(∼ ∆)L∪(∼ ∆′)L∪ {zA1(∼A)L,yA2A′R,x3(B⊸C)L} ∪DNEα
である IPSiαiの存在
α1に帰納法の仮定を 適用し て 、 T N(βi) = ΓL∪(∼ ∆)L∪ {zA1(∼A)L,x1BR} ∪ DNEα1 である IPSiβiが取れる 。 同様に α2に帰納法の仮定を 適用し て 、 T N(γi) = Γ′L ∪(∼ ∆′)L∪ {yA2A′R,x2CL} ∪DNEα2 である IPSiγiが取れる 。 よ っ て 、 以下のよ う にαi′を 構成でき る 。
βi γi αi′ L⊸
最後に、 DNEα = DNEα1 ∪DNEα2な ので、 αi =αi′である 。
3. T N(αi)= ΓL∪Γ′L∪(∼∆)L∪(∼ ∆′)L∪ {zA1(∼A)R,yA2(∼A′)L,x3(B⊸C)L} ∪DNE である IPSiαiの存在
T N(βi) = ΓL ∪(∼ ∆)L ∪ {zA1(∼A)L,x1BR} ∪ DNEα1 であ る IPSi βi が取れ る 。 同様に α2 に 帰納法の仮定を 適用し て 、 T N(γi) = Γ′L ∪(∼ ∆′)L ∪ {zA2(∼A′)L,x2CL} ∪DNEα2である IPSiγiが取れる 。 よ っ て 、 以下のよ う に αi′を 構成でき る 。
βi γi
αi′′ L⊸ αi′ R0
最後に、 DNEα = DNEα1 ∪DNEα2な ので、 αi =αi′である 。
• 最後にR⊸規則で導出さ れたと き
T N(α′) = ΓL ∪∆R ∪ {yAAR,x1BL,x2CR}であ る IPSc α′に R0規則を 適用し て 、 T N(α) = ΓL ∪∆R∪ {yAAR,x3(B⊸C)R}である IPScαを 構成し たと する 。 こ のと き 、 ３ つのIPSiの存在を 示す。
1. T N(αi)= ΓL∪(∼∆)L∪ {yAAR,z3(∼(B⊸C))L} ∪DNEαである IPSiαiの存在 α′にR⊸に関する 可逆性を 適用し て、T N(β)= ΓL∪ΓAL∪∆R∪{yaaR,x1BL,x2CR} である IPScβが取れる 。 βに 帰納法の仮定を 適用し て 、 T N(βi) = ΓL∪ ΓAL∪(∼∆)L∪ {za(∼a)L,x1BL,x2CR} ∪DNEβ である βiが取れたと する 。 こ のと き 、 以下のよ う に求めるαi構成でき る 。
βi
βi1 R⊸ ({x0},∅,{(x0,0L)}) βi2
L⊸ ({xa1,xa2},{(xa1,xa2)},{(xa1,aL),(xa2,aR)})
αi′ L⊸
... αi
T N(βi1)= ΓL∪ΓAL∪(∼∆)L∪ {za(∼a)L,x3(B⊸C)R} ∪DNEβ T N(βi2)= ΓL∪ΓAL∪(∼∆)L∪ {za(∼a)L,z3(∼(B⊸C))L} ∪DNEβ T N(αi′
)= ΓL∪ΓAL∪(∼∆)L∪ {ya′aR,z3(∼(B⊸C))L} ∪DNEβ∪ {x(∼∼a⊸a)L} DNEα = DNEβ∪ {x(∼∼a⊸a)L}な ので、 αi = αi′である 。
2. T N(αi)= ΓL∪(∼∆)L∪ {zA(∼A)L,x3(B⊸C)R} ∪DNEαである IPSiαiの存在 α′に帰納法の仮定を 適用し て、T N(α′i)= ΓL∪(∼∆)L∪{zA(∼A)L,x1BL,x2CR}∪
DNEα′である IPSiα′iが取れる 。 よ っ て 、 こ れにR⊸規則を 適用し て 、 求める αiが取れる 。
3. T N(αi)= ΓL∪(∼∆)L∪ {zA(∼A)L,z3(∼(B⊸C))L} ∪DNEαである IPSiαiの存在 α′に帰納法の仮定を 適用し て、T N(α′i)= ΓL∪(∼∆)L∪{zA(∼A)L,x1BL,x2CR}∪
DNEα′である IPSiα′iが取れる 。 よ っ て 、 以下のよ う に求める αi構成で き る 。
α′i β αi L⊸ こ こ で、 T N(β)= {y00L,z0R}である 。
し たがっ て 、 ∆を 高々 １ つの節点と すれば、 以下の定理が得ら れる 。
定理. T NR(α)が高々１ つの節点から なるIPScαが存在する なら ば、T N(αi)=T N(α)∪
DNEαである IPSiαiが存在する 。 ただし 、 DNE ={x(∼∼p⊸p)L|(x2,pR)∈Lα}である 。 こ こ で、 x2 7−→ x<Vαは単射である 。
次に、 分裂定理のよ う な 補題を 示す。 分裂定理のよ う に具体的に分裂可能な 節点