証明論 (3): カット除去定理の証明 (1) [証明論]

証明論 (2) で言及したカット除去定理を証明する。

まず、「ミックス」と呼ばれる新たな証明ルールを導入する。
\[\cfrac{\Gamma \rightarrow \Theta \qquad \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}\] ここで $\Theta^*, \Delta^*$ はそれぞれ、$\Theta, \Delta$ から論理式 $\mathfrak{M}$ を除いたものとする（ここで $\mathfrak{M}$ は「ミックス式」と呼ばれる）。ミックスとカットは、交換・縮約・薄めを何回か適用することにより、たがいに変換可能である。

演習：ミックスとカットがたがいに変換可能であることを確かめよ。

つぎに、証明の複雑さを測るふたつの尺度である次数 $dg$ および階数 $rk$ を導入する。$dg$ とはミックス式の論理演算子の個数を表し、$rk$ はミックスが適用された式から数えて最後にミックス式が現れるシーケントの個数である。ここで $rk_l, rk_r$ をそれぞれミックスが適用された式より左側／右側の階数とし、$rk=rk_l+rk_r$ とする。ミックスが現れる証明においてはミックスが適用された式の直前にかならずミックス式が現れるので $rk > 1$ となる。ミックスが用いられる証明を $\Pi$ とするとその証明の次数および階数はそれぞれ $gd(\Pi), rk(\Pi)$ で表される。また、ミックス式に同じ論理演算子が複数回現れる場合、それぞれをひとつとして数える。

例：つぎの証明の次数は 1 であり階数は 3 である。
\[
\cfrac{\cfrac{\mathfrak{F}(\mathfrak{a}) \rightarrow \mathfrak{F}(\mathfrak{a})}{\mathfrak{F}(\mathfrak{a}) \rightarrow \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})} \qquad \cfrac{\exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})}{\neg \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}), \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow}}{\mathfrak{F}(\mathfrak{a}), \neg \exists \mathfrak{x} \mathfrak{F}(\mathfrak{x}) \rightarrow}
\] 上で述べたとおり、カットとミックスはたがいに変換可能なので、カット除去定理を証明するには任意の証明からミックスが取り除けることを示せばよい。そのような方針のもと、次数と階数にかんする二重帰納法でカット除去定理を証明する。

Case 1: $rk=2$ の場合
Case 1.1.1: ミックス式が始式として、つまり $\mathfrak{M} \rightarrow \mathfrak{M}$ のかたちでミックスが適用される左の式に現れる場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\mathfrak{M} \rightarrow \mathfrak{M} \qquad \Delta \rightarrow \Lambda}{\mathfrak{M}, \Delta^* \rightarrow \Lambda}
\] これは、以下のようにミックスを用いず証明可能である。
\[
\cfrac{\cfrac{\Delta \rightarrow \Lambda}{\vdots}}{\mathfrak{M}, \Delta^* \rightarrow \Lambda}
\] ここで $\vdots$ によって省略された箇所は、何回かの交換によってミックス式 $\mathfrak{M}$ を $\Delta$ の外に掃き出し、縮約で複数のミックス式をひとつにまとめている。
Case: 1.1.2 ミックス式が始式として、つまり $\mathfrak{M} \rightarrow \mathfrak{M}$ のかたちでミックスが適用される右の式に現れる場合
Case 1.1 の場合と同様に証明する。

Case 1.2: ミックス式が $\mathfrak{A} \& \mathfrak{B}$ というかたちの場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\cfrac{\Gamma \rightarrow \Theta, \mathfrak{A} \qquad \Gamma \rightarrow \Theta, \mathfrak{B}}{\Gamma \rightarrow \Theta, \mathfrak{A} \& \mathfrak{B}} \qquad \cfrac{\mathfrak{A}, \Delta \rightarrow \Lambda}{\mathfrak{A} \& \mathfrak{B}, \Delta \rightarrow \Lambda}}{\Gamma, \Delta \rightarrow \Theta, \Lambda}
\] 帰納法の仮定により、以下はミックスなしで証明可能である。
\[
\cfrac{\Gamma \rightarrow \Theta, \mathfrak{A} \qquad \mathfrak{A}, \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}
\] こうして得られた $\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda$ に薄めと交換を何回か適用すると目的の式である $\Gamma, \Delta \rightarrow \Theta, \Lambda$ が得られる。

Case 1.3: ミックス式が $\mathfrak{A} \vee \mathfrak{B}$ というかたちの場合
Case 1.2 の場合と同様に証明する。

Case 1.4: ミックス式が $\forall \mathfrak{x} \mathfrak{F}(\mathfrak{x})$ というかたちの場合
この場合、ミックスは以下のかたちとなる。
\[
\cfrac{\cfrac{\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{a})}{\Gamma \rightarrow \Theta, \forall \mathfrak{x} \mathfrak{F}(\mathfrak{x})} \qquad \cfrac{\mathfrak{F}(\mathfrak{b}), \Delta \rightarrow \Lambda}{\forall \mathfrak{x} \mathfrak{F}(\mathfrak{x}), \Delta \rightarrow \Lambda}}{\Gamma, \Delta \rightarrow \Theta, \Lambda}
\] ここで、「$\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{a})$ が証明可能であるなら $\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{b})$ も証明可能である」という補題を用いる。すると、帰納法の仮定により、以下がミックスなしで証明可能である。
\[
\cfrac{\Gamma \rightarrow \Theta, \mathfrak{F}(\mathfrak{b}) \qquad \mathfrak{F}(\mathfrak{b}), \Delta \rightarrow \Lambda}{\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda}
\] こうして得られた $\Gamma, \Delta^* \rightarrow \Theta^*, \Lambda$ に、Case 1.2 の場合と同様に薄めと交換を何回か適用して目的の式である $\Gamma, \Delta \rightarrow \Theta, \Lambda$ を得る。

演習：上で用いた補題を証明せよ。

Case 1.5: ミックス式が $\exists \mathfrak{x} \mathfrak{F}(\mathfrak{x})$ というかたちの場合
Case 1.4 の場合と同様に証明する。

演習：ミックス式が $\mathfrak{A} \supset \mathfrak{B}$ というかたちを持つ場合と $\neg \mathfrak{A}$ というかたちを持つ場合のそれぞれ証明せよ。

次回は $rk(\Pi)>2$ の場合を証明する。