線形論理

組 $(|A|,\ h(\pi_1)+h(\pi_2))$ に関する辞書式順序の帰納法による。$\pi_1,\pi_2$ の最後の規則を $r_1,r_2$ とし、場合を分ける。
(i) 一方が公理． $\pi_1$ が $\vdash A^\perp,A$ なら $\Gamma=A^\perp$ で、求める $\vdash A^\perp,\Delta$ は $\pi_2$ の結論そのものである。$\pi_2$ が公理の場合も同じである。
(ii) カットする論理式が $r_1$ の主論理式でない． $r_1$ を後回しにする。たとえば $r_1$ が $\text{⅋}$ で $\pi_1$ が $\pi_1'\colon\vdash\Gamma',C,D,A$ から $\vdash\Gamma',C\mathbin{\text{⅋}}D,A$ を導くなら、$\pi_1'$ と $\pi_2$ に帰納法の仮定（高さの和が減る）を使って $\vdash\Gamma',C,D,\Delta$ をカットなしで得て、$\text{⅋}$ 規則で $\vdash\Gamma',C\mathbin{\text{⅋}}D,\Delta$ を得る。

• $A=B\otimes C$：$\pi_1$ は $\vdash\Gamma_1,B$ と $\vdash\Gamma_2,C$ から、$\pi_2$ は $\vdash\Delta,B^\perp,C^\perp$ から作られる。$\vdash\Gamma_1,B$ と $\vdash\Delta,B^\perp,C^\perp$ に帰納法の仮定を使い（$|B|<|A|$）$\vdash\Gamma_1,\Delta,C^\perp$ を得て、これと $\vdash\Gamma_2,C$ に帰納法の仮定を使い（$|C|<|A|$）$\vdash\Gamma_1,\Gamma_2,\Delta$ を得る。
• $A=\mathbf 1$：$\Gamma$ は空で、$\pi_2$ は $\vdash\Delta$ から $\perp$ 規則で $\vdash\Delta,\perp$ を導く。求める $\vdash\Delta$ はその前提である。
• $A=B\mathbin{\&}C$：$\pi_1$ は $\vdash\Gamma,B$ と $\vdash\Gamma,C$ から、$\pi_2$ はたとえば $\vdash\Delta,B^\perp$ から $\oplus_1$ で作られる。$\vdash\Gamma,B$ と $\vdash\Delta,B^\perp$ に帰納法の仮定を使えばよい。
• $A=\top$：$A^\perp=\mathbf 0$ を主論理式とする規則はないので、この場合は起こらない。
  どの場合も、帰納法の仮定を使う先は $|A|$ が小さいか、$|A|$ が同じで高さの和が小さい。$\square$

導出に含まれるカットの個数に関する帰納法による。カットがあれば、その上にカットがないものを 1 つ選ぶ。その 2 つの前提の導出はカットなしなので、lem-ll-one-cut によりこのカットをカットなしの導出に置き換えられる。カットが 1 つ減る。$\square$

1. cut 以外の規則では、前提に現れる論理式は結論に現れる論理式か、主論理式の直接の部分論理式である。公理と $\top$ の規則も前提をもたないので、導出を下から上へたどる帰納法で結論を得る。
2. シークエント $\vdash\Gamma$ の 大きさ を、$\Gamma$ の論理式の大きさの和とする。$\mathbf{MALL}$ の cut 以外の規則では、各前提の大きさは結論より真に小さい（主論理式の結合子か定数が 1 つ消え、$\otimes$ ではさらに他方の前提の部分も消える）。thm-ll-cut-elimination により、$\vdash\Gamma$ が導出可能であることは、カットなしの導出があることと同じである。与えられたシークエントの下の規則としてありうるもの（主論理式の選び方と、$\otimes$ での文脈の分け方）は有限個しかなく、前提は真に小さいので、すべての可能性を再帰的に試す手続きは必ず止まる。公理か $\top$ か $\mathbf 1$ の規則に行き着く枝だけで木が作れるかどうかを調べればよい。$\square$

導出に関する帰納法による。公理 $\vdash A,A^\perp$ では $n_p=n_p(A)+n_{\bar p}(A)=n_{\bar p}$。$\otimes$ と $\text{⅋}$ の規則は、前提の多重集合の論理式をつなぐだけなので個数を保つ（$\otimes$ では 2 つの前提の個数の和になる）。$\mathbf 1$ と $\perp$ は原子を含まない。cut では、前提 $\vdash\Gamma,A$ と $\vdash\Delta,A^\perp$ で釣り合いが成り立つとすると、結論で消える $A,A^\perp$ に含まれる $p$ の個数は $n_p(A)+n_{\bar p}(A)$、$p^\perp$ の個数は $n_{\bar p}(A)+n_p(A)$ で等しいので、結論でも釣り合いが成り立つ。$\square$

2 つのシークエントは $\vdash p^\perp\mathbin{\text{⅋}}(p\otimes p)$ と $\vdash(p^\perp\mathbin{\text{⅋}}q^\perp)\mathbin{\text{⅋}}p$ で、$\mathbf{MLL}$ の論理式からなる。$\mathbf{MALL}$ で導出できたとすると、thm-ll-cut-elimination によりカットなしの導出があり、cor-ll-decidable の 1 によりそこに現れる論理式はすべて結論の部分論理式なので、$\mathbin{\&},\oplus,\top,\mathbf 0$ を含まない。したがってその導出は $\mathbf{MLL}$ の導出である。ところが前者は $n_p=2$、$n_{\bar p}=1$、後者は $n_q=0$、$n_{\bar q}=1$ なので、thm-ll-balance に反する。$\square$

$\mathbf{LJ}_{\land\to}$ の導出に関する帰納法による。$\Gamma=A_1,\dots,A_n$ のとき $?\Gamma^{\ast\perp}$ で $?(A_1^\ast)^\perp,\dots,?(A_n^\ast)^\perp$ を表す。要になるのは次の 2 点である。左辺の論理式はすべて $?$ が付いた形で現れるので、左の弱化・縮約は $?\mathrm w$・$?\mathrm c$ で写せる。また、文脈がすべて $?$ で始まるので、$!$ 規則がいつでも使える。

• 始シークエント $A\Rightarrow A$：$\vdash(A^\ast)^\perp,A^\ast$ に $?\mathrm d$。
• カット（$\Gamma\Rightarrow A$ と $A,\Pi\Rightarrow C$ から $\Gamma,\Pi\Rightarrow C$）：$\vdash ?\Gamma^{\ast\perp},A^\ast$ に $!$ 規則を使って $\vdash ?\Gamma^{\ast\perp},!A^\ast$。これと $\vdash ?(A^\ast)^\perp,?\Pi^{\ast\perp},C^\ast$ を、$(!A^\ast)^\perp=?(A^\ast)^\perp$ でカットする。
• $\to$ の右規則（$A,\Gamma\Rightarrow B$ から $\Gamma\Rightarrow A\to B$）：$\vdash ?(A^\ast)^\perp,?\Gamma^{\ast\perp},B^\ast$ に $\text{⅋}$ 規則を使えば、$?(A^\ast)^\perp\mathbin{\text{⅋}}B^\ast=\,!A^\ast\multimap B^\ast$ である。
• $\land$ の右規則：2 つの前提 $\vdash ?\Gamma^{\ast\perp},A^\ast$ と $\vdash ?\Gamma^{\ast\perp},B^\ast$ は文脈が同じなので、$\&$ 規則で $\vdash ?\Gamma^{\ast\perp},A^\ast\mathbin{\&}B^\ast$。
  $\land$ と $\to$ の左規則を開く

  $\land$ の左規則（$A,\Gamma\Rightarrow C$ から $A\land B,\Gamma\Rightarrow C$）：$((A\land B)^\ast)^\perp=(A^\ast)^\perp\oplus(B^\ast)^\perp$ である。$\vdash(A^\ast)^\perp,A^\ast$ から $\oplus_1$ で $\vdash(A^\ast)^\perp\oplus(B^\ast)^\perp,A^\ast$、$?\mathrm d$ で $\vdash ?((A^\ast)^\perp\oplus(B^\ast)^\perp),A^\ast$、$!$ 規則で $\vdash ?((A^\ast)^\perp\oplus(B^\ast)^\perp),!A^\ast$ を得て、前提 $\vdash ?(A^\ast)^\perp,?\Gamma^{\ast\perp},C^\ast$ と $!A^\ast$ でカットする。もう一方の形（$B,\Gamma\Rightarrow C$ から）は $\oplus_2$ を使う。

  $\to$ の左規則（$\Gamma\Rightarrow A$ と $B,\Pi\Rightarrow C$ から $A\to B,\Gamma,\Pi\Rightarrow C$）：$((A\to B)^\ast)^\perp=(?(A^\ast)^\perp\mathbin{\text{⅋}}B^\ast)^\perp=\,!A^\ast\otimes(B^\ast)^\perp$ である。$\vdash ?\Gamma^{\ast\perp},A^\ast$ から $!$ 規則で $\vdash ?\Gamma^{\ast\perp},!A^\ast$、これと $\vdash(B^\ast)^\perp,B^\ast$ を $\otimes$ でつないで $\vdash ?\Gamma^{\ast\perp},!A^\ast\otimes(B^\ast)^\perp,B^\ast$、$?\mathrm d$ で $\vdash ?\Gamma^{\ast\perp},?(!A^\ast\otimes(B^\ast)^\perp),B^\ast$ を得る。$B^\ast$ 以外はすべて $?$ で始まるので $!$ 規則で $\vdash ?\Gamma^{\ast\perp},?(!A^\ast\otimes(B^\ast)^\perp),!B^\ast$ とし、前提 $\vdash ?(B^\ast)^\perp,?\Pi^{\ast\perp},C^\ast$ と $!B^\ast$ でカットすれば $\vdash ?((A\to B)^\ast)^\perp,?\Gamma^{\ast\perp},?\Pi^{\ast\perp},C^\ast$ である。

  左の弱化・縮約は $?\mathrm w$・$?\mathrm c$、交換は多重集合なので何もしなくてよい。$\square$