この本で線形論理の勉強をしているよ。
加法も乗法も量化子も指数も全部入れたフル線形論理のカット除去定理の解説がある。自分で証明を書いていてちょっとポイントがわかった。
鹿島先生の『数理論理学』では、LKのカット除去定理の証明のために「拡張カット」というのが使われている。
これは弱化があるためにカット除去手続きが上手くいかない部分があるからである。詳しく図を載せたいけど面倒くさいのでそのうち記事をアップデートします。
しかし線形論理は構造規則が様相論理式に制限されているので、様相のない部分（つまりMALL）ではカット除去が容易にできる。様相論理式だけのための拡張カットのようなものを定義してその場合特有のカット除去を"Lectures on Linear Logic"ではしている。ただし弱化は！と？で左右別々にあるので、拡張カットも左右非対称になる。
わかりにくいのでマジでそのうち図を載せます。
