カット除去定理に関するいくつか
証明木を描くのがあまりにも面倒なので結論だけ書く．
数学における証明と真理 様相論理と数学基礎論の3章を参考にすること．
定義
様相論理式の集合$ \Gammaについて，$ \Box\Gamma \coloneqq \{ \Box \varphi \mid \varphi \in \Gamma \}
多重集合
通常の集合に多重度という概念を入れて重複を許したものを多重集合という．
例えば$ \{\varphi,\varphi,\psi\}は
集合としては$ \{\varphi,\psi\}だが
多重集合としては$ \varphiの多重度2，$ \psiの多重度1とする．
順番は無視する．
シークエント
多重集合$ \Gamma,\Deltaについて，$ \Gamma \Rightarrow \Deltaをシークエントという．
$ \Gamma,\Deltaを多重集合としたことによって，シークエント計算の交換規則は考えなくても良い．
$ \Gamma \Rightarrow \Deltaは論理式$ \bigwedge \Gamma \to \bigvee \Deltaに翻訳可能．
ただし$ \bigwedge \emptyset \coloneqq \top, \bigvee \emptyset \coloneqq \botとする．
$ \LambdaのHilbert流演繹体系$ \mathcal{H}_\Lambda
シーケント計算の始式規則，構造規則，論理規則，$ \Lambdaの規則を全て合わせた規則によるシークエント計算の体型を$ \mathcal{S}_\Lambdaとする．
$ \mathcal{S}_\Lambdaにカット規則を合わせた計算体型を$ \mathcal{S}^c_\Lambdaとする
補題
$ \mathcal{S}^c_\mathbf{P}は始式規則，構造規則，論理規則，カット規則を全て合わせた体系を．命題論理のカット規則ありのシーケント計算とする．
$ \vdash_{\mathcal{H}_\mathbf{P}} \varphiなら$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \varphi
proof:
命題論理のHilbert流演繹体系$ \mathcal{H}_\mathbf{P}はŁukasiewiczの3公理図式，一様代入，モーダス・ポネンスの3要素で構成される．
Łukasiewiczの3公理図式を$ \mathsf{A_1},\mathsf{A_2},\mathsf{A_3}とすると$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \mathsf{A_1}，$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \mathsf{A_2}，$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \mathsf{A_3}である．
実際にはカット規則無しで証明可能．
$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \varphiと$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \varphi \to \psiを仮定すると$ \vdash_{\mathcal{S}^c_\mathbf{P}} \psiが証明可能なのでモーダス・ポネンスも証明可能．
一様代入則はほとんど自明なので省略
以上よりHilbert流演繹体系での$ \varphiの証明の列$ \varphi_1,\dots,\varphi_n = \varphiに対応する証明木をシークエント計算でも構成可能．❏
系
$ \Lambda \coloneqq \bf K,KT,S4,S5として$ \vdash_{\mathcal{S}^c_\mathbf{P}} \varphiなら$ \vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \varphi
当然ながら，様相論理のシークエント計算は命題論理のシーケント計算よりも真に強い．
定理: 3.1.2
$ \Lambda \coloneqq \bf K,KT,S4,S5とする．
1. $ \vdash_{\mathcal{H}_\Lambda} \varphiなら$ \vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \varphi
2. $ \vdash_{\mathcal{S}^c_\Lambda} \Gamma \Rightarrow \Deltaなら$ \vdash_{\mathcal{H}_\Lambda} \bigwedge \Gamma \to \bigvee \Delta
proof 1:
$ \varphiがトートロジーなら（すなわち$ \varphi \in \mathsf{Taut}）$ \vdash_{\mathcal{H}_\mathbf{P}} \varphiであるので，↑の補題より，$ \vdash_{\mathcal{S}^c_\mathbf{P}} \Rightarrow \varphi
様相論理のHilbert流演繹体系$ \mathcal{H}_\Lambdaは古典命題論理のトートロジー，一様代入，必然化，モーダスポネンスと，各々の公理$ \mathsf{K,T,4,B}から構成される．
系:1
3.1.2より直ちに，$ \vdash_{\mathcal{H}_\Lambda} \varphi$ \iff$ \vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \varphi
定理: カット除去定理
$ \Lambda \coloneqq \bf K,KT,S4とする．
$ \vdash_{\mathcal{S}^c_\Lambda} \Gamma \Rightarrow \Deltaなら$ \vdash_{\mathcal{S}_\Lambda} \Gamma \Rightarrow \Delta
$ \Lambda \coloneqq \bf S5では成り立たない．定理4
系:2
$ \not\vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \bot
証明
$ \vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \botと仮定して背理法．
系:3
$ \not\vdash_{\mathcal{H}_\Lambda} \bot
証明
3.1.2.1の対偶$ \not\vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \varphiなら$ \not\vdash_{\mathcal{H}_\Lambda} \varphi．系2より$ \not\vdash_{\mathcal{S}^c_\Lambda} \Rightarrow \bot．したがって$ \not\vdash_{\mathcal{H}_\Lambda} \bot．❏
定理:4
様相論理の公理Bはカット規則無しでは証明できない．
すなわち，$ \vdash_{\mathcal{S}_\mathbf{S5}^c}\mathsf{B}だが，$ \not\vdash_{\mathcal{S}_\mathbf{S5}}\mathsf{B}
$ \mathsf{B} \equiv p \to \Box\Diamond p \equiv p \to \Box\lnot\Box\lnot p
proof:
$ \Rightarrow \to規則を適応した$ p \Rightarrow \Box\lnot\Box\lnot pがカット規則なしで証明可能であるとする．
カット規則が無いとき，$ p \Rightarrow \Box\lnot\Box\lnot pに適応できる規則は弱化規則と縮約規則のみ．
$ p \Rightarrow \Box\lnot\Box\lnot pがカット規則なしで証明可能であるとする．
弱化規則を適応すると$ p \Rightarrowまたは$ \Rightarrow \Box\lnot\Box\lnot pが証明可能でなければならない．
$ \Rightarrow \Box\lnot\Box\lnot pは更に$ \lnot p \Rightarrowが証明可能でなければならない．
Hilbert流演繹体系に直すと，$ \vdash_{\mathcal{H}_\mathbf{S5}} p \to \botまたは$ \vdash_{\mathcal{H}_\mathbf{S5}} \lnot p \to \botである．
これは矛盾．
縮約規則を適応すると$ p,p \Rightarrow \Box\lnot\Box\lnot pまたは$ p \Rightarrow \Box\lnot\Box\lnot p,\Box\lnot\Box\lnot pのどちらかで，どちらの場合でも適応できる規則は弱化規則または縮約規則しかない．
弱化規則を適応すると↑の議論より矛盾．縮約規則を適応すると結局無限ループに．
よって，$ p \Rightarrow \Box\lnot\Box\lnot pはカット規則なしでは証明不可能．❏