カット除去定理

$\Gamma'$ の文を $\mathrm{WL}$ で左端に、$\Delta'$ の文を $\mathrm{WR}$ で右端に 1 つずつ付け加える。$\Gamma$ の部分にある各文 $D$ は付け加えた部分にもあるので、交換で 2 つの $D$ を隣り合わせて $\mathrm{CL}$ で 1 つにできる。これを繰り返すと左辺は付け加えた部分だけになり、交換で $\Gamma'$ の順に並べ替えられる。右辺も同様である。$\square$

1：$D$ の各規則が置き換えの後も同じ規則であることを確かめる。始シークエント、構造規則、カット、命題の規則は、置き換えが論理記号と交換するので明らかである。$\forall\mathrm L$ と $\exists\mathrm R$ の閉項 $s$ は閉項 $s[t/a]$ に替わり、$t$ が閉項なので $(A(s))[t/a]=(A[t/a])(s[t/a])$ である。$\forall\mathrm R$ と $\exists\mathrm L$ の固有変数 $b$ は仮定により $b\ne a$ なので、$(A(b))[t/a]=(A[t/a])(b)$ である。$b$ は結論に現れず $t$ にも現れないので、置き換えた後の結論にも現れない。木の形は変わらないので高さも同じである。
2：$h$ についての帰納法による。最後の規則が $\forall\mathrm R$、$\exists\mathrm L$ でなければ、各前提の導出に帰納法の仮定を当てて同じ規則を使えばよい。最後の規則が固有変数 $b$ の $\forall\mathrm R$ で、前提が $\Gamma\Rightarrow\Delta,A(b)$ だとする（$\exists\mathrm L$ も同様）。$F\cup\{b\}$ に属さず $S$ に現れない定数記号 $c$ をとる。帰納法の仮定により、前提の導出 $D_0'$ で固有変数が $F\cup\{b,c\}$ に属さないものがある。$b$ は $\Gamma,\Delta,A(x)$ に現れないので、1 により $D_0'[c/b]$ は $\Gamma\Rightarrow\Delta,A(c)$ の導出で、高さは変わらない。$c$ は $S$ に現れないので、固有変数 $c$ の $\forall\mathrm R$ で $S$ が得られる。$\square$

組 $(\deg A,\ h_1+h_2)$（$h_i$ は $D_i$ の高さ）についての辞書式順序の帰納法で示す。つまり、次数が $\deg A$ より小さい文については、どんな高さのカットのない導出についても主張が成り立つと仮定し、次数が $\deg A$ の文については、高さの和が $h_1+h_2$ より小さい導出について成り立つと仮定する。目標の組を $G:=(X\cup U^-,\ Y^-\cup V)$ とし、「$G$ より小さい組」とは両成分がそれぞれ $G$ の成分に含まれる組をいう。弱化により、$G$ より小さい組が $\vdash_0$ ならよい。
場合 1：どちらかが始シークエント。 $D_1$ が始シークエント $B\Rightarrow B$ なら、$A\in Y=\{B\}$ より $B=A$ で、$A\in U$ なので $G=(\{A\}\cup U^-,V)=(U,V)$ である。これは $D_2$ そのものである。$D_2$ が始シークエントなら同様に $G=(X,Y)$ で、$D_1$ そのものである。
場合 2：$D_1$ の最後の規則 $r$ が、主論理式 $A$ の右の論理規則ではない。 $r$ が $\forall\mathrm R$ か $\exists\mathrm L$ なら、lem-ce-subst の 2 と 1 で、前提の導出ごと $r$ の固有変数を $\Gamma\Rightarrow\Delta$ にも $\Pi\Rightarrow\Lambda$ にも現れない定数記号 $c$ に取り替えておく（高さは変わらない）。$r$ の各前提 $P$ の集合の組を $(X_P,Y_P)$ とする。$P$ の導出の高さは $h_1$ より小さい。このとき
$$ \vdash_0X_P\cup U^-\Rightarrow Y_P^-\cup V\qquad(\ast) $$
が成り立つ。$A\in Y_P$ なら、$P$ の導出と $D_2$ に帰納法の仮定（次数は同じ、高さの和は小さい）を当てればよい。$A\notin Y_P$ なら $Y_P^-=Y_P$ なので、$P$ そのものに弱化を当てればよい。

• $r$ が構造規則なら $X_P\subset X$、$Y_P\subset Y$ なので、$(\ast)$ の組は $G$ より小さい。
• $r$ が論理規則なら、前提の組は「文脈の集合」に副論理式を加えたもので、文脈の集合は結論の文脈の集合に含まれる。$(\ast)$ に弱化で右の副論理式を加え直すと、前提と同じ副論理式をもち、文脈に $U^-$ と $V$ を加え右の文脈から $A$ を除いた組が得られる。そこに同じ規則 $r$ を当てる。得られる結論の組は、$r$ の結論の文脈から右辺の $A$ を除き $U^-$ と $V$ を加え、主論理式を加えたものである。主論理式は、左にあれば $X$ に属し、右にあれば仮定により $A$ でないので $Y^-$ に属する。よって結論の組は $G$ より小さい。固有変数 $c$ は $G$ の文に現れないので、条件は満たされる。

場合 3：$D_2$ の最後の規則が、主論理式 $A$ の左の論理規則ではない。 場合 2 と左右を入れ替えて同じように示せる。
場合 4：$D_1$ の最後の規則は主論理式 $A$ の右の規則、$D_2$ の最後の規則は主論理式 $A$ の左の規則。 $W:=X\cup U^-$、$Z:=Y^-\cup V$ とおき、$\vdash_0W\Rightarrow Z$ を示す。まず次の 2 つを確かめる。

• (i) $D_1$ の最後の規則の各前提 $P$ について、$P$ の左辺の副論理式の集合を $E_{\mathrm L}$、右辺の副論理式の集合を $E_{\mathrm R}$ とすると、$\vdash_0W\cup E_{\mathrm L}\Rightarrow Z\cup E_{\mathrm R}$。
• (ii) $D_2$ の最後の規則の各前提についても、同じ形が成り立つ。
  (i) は場合 2 の $(\ast)$ と同じ議論である。前提の右の文脈に $A$ があれば帰納法の仮定（高さの和が小さい）で取り除き、なければそのまま弱化する。副論理式は $A$ の真の部分論理式で $A$ とは異なるので、取り除かれずに残る。(ii) も、前提の左の文脈から $A$ を取り除いて同様に示せる。
  そのうえで、$A$ の形に応じて、副論理式についての混合補題（次数が小さい）でつなぐ。$A=B\land C$ で $D_2$ の最後の規則が $B$ を副論理式とする $\land\mathrm L$ なら、(i) から $\vdash_0W\Rightarrow Z\cup\{B\}$、(ii) から $\vdash_0W\cup\{B\}\Rightarrow Z$ である。この 2 つのカットのない導出に、$\deg B<\deg A$ の帰納法の仮定を当てると、$\vdash_0W\cup\bigl((W\cup\{B\})\setminus\{B\}\bigr)\Rightarrow\bigl((Z\cup\{B\})\setminus\{B\}\bigr)\cup Z$ である。この組は $(W,Z)$ より小さい。
  $A=\forall x\,B(x)$ のときは、$D_1$ の最後の規則が固有変数 $a$ の $\forall\mathrm R$ で前提が $\Gamma\Rightarrow\Delta_0,B(a)$、$D_2$ の最後の規則が閉項 $t$ の $\forall\mathrm L$ で前提が $B(t),\Pi_0\Rightarrow\Lambda$ である。lem-ce-subst の 2 で前提の導出の固有変数を $a$ と $t$ の定数記号から外し、1 で $a$ を $t$ に置き換える。$a$ は $\Gamma,\Delta_0,B(x)$ に現れないので、$\Gamma\Rightarrow\Delta_0,B(t)$ の、高さが $h_1$ より小さいカットのない導出が得られる。これを前提として (i) を使うと $\vdash_0W\Rightarrow Z\cup\{B(t)\}$、(ii) から $\vdash_0W\cup\{B(t)\}\Rightarrow Z$ である。$\deg B(t)<\deg A$ なので、$\land$ の場合と同じく帰納法の仮定で $\vdash_0W\Rightarrow Z$ を得る。
  残りの論理記号の場合を開く

  $\lor$：$D_1$ が $B$（または $C$）を副論理式とする $\lor\mathrm R$ なら、(i) から $\vdash_0W\Rightarrow Z\cup\{B\}$、$\lor\mathrm L$ の $B$ の前提について (ii) から $\vdash_0W\cup\{B\}\Rightarrow Z$ で、$B$ について混合する。

  $\lnot$：$A=\lnot B$ なら、$\lnot\mathrm R$ の副論理式 $B$ は左にあるので (i) から $\vdash_0W\cup\{B\}\Rightarrow Z$、$\lnot\mathrm L$ の副論理式 $B$ は右にあるので (ii) から $\vdash_0W\Rightarrow Z\cup\{B\}$ である。後者を左に、前者を右に置いて $B$ について混合する。

  $\to$：$A=B\to C$ なら、${\to}\mathrm R$ の前提について (i) から $\vdash_0W\cup\{B\}\Rightarrow Z\cup\{C\}$、${\to}\mathrm L$ の 2 つの前提について (ii) から $\vdash_0W\Rightarrow Z\cup\{B\}$ と $\vdash_0W\cup\{C\}\Rightarrow Z$ である。1 つ目と 3 つ目を $C$ について混合すると、組 $\bigl(W\cup\{B\}\cup((W\cup\{C\})\setminus\{C\}),\ ((Z\cup\{C\})\setminus\{C\})\cup Z\bigr)$ は $(W\cup\{B\},Z)$ より小さいので $\vdash_0W\cup\{B\}\Rightarrow Z$ である。これと 2 つ目を $B$ について混合して $\vdash_0W\Rightarrow Z$ を得る。$\deg B,\deg C<\deg A$ である。

  $\exists$：$A=\exists x\,B(x)$ なら、$D_1$ は閉項 $t$ の $\exists\mathrm R$ で前提 $\Gamma\Rightarrow\Delta_0,B(t)$、$D_2$ は固有変数 $a$ の $\exists\mathrm L$ で前提 $B(a),\Pi_0\Rightarrow\Lambda$ である。$\forall$ の場合と左右を入れ替え、$D_2$ の前提の導出で $a$ を $t$ に置き換える。(i) から $\vdash_0W\Rightarrow Z\cup\{B(t)\}$、(ii) から $\vdash_0W\cup\{B(t)\}\Rightarrow Z$ で、$B(t)$ について混合する。

  場合 1〜4 で、すべての組み合わせが尽くされている。場合 2・3 に当たらなければ、両方の最後の規則が $A$ を主論理式とする論理規則で、$A$ の右の規則と左の規則の組である。$\square$

導出 $D$ に含まれるカットの個数についての帰納法による。カットがなければよい。カットがあれば、それより上にカットを含まないカット（導出は有限なので存在する）を 1 つとる。その前提 $\Gamma\Rightarrow\Delta,A$ と $A,\Pi\Rightarrow\Lambda$ はカットのない導出をもつ。lem-ce-mix により
$$ \vdash_0|\Gamma|\cup|\Pi|^-\Rightarrow|\Delta,A|^-\cup|\Lambda| $$
であり、この組は $(|\Gamma,\Pi|,|\Delta,\Lambda|)$ より小さいので、lem-ce-structural によりカットの結論 $\Gamma,\Pi\Rightarrow\Delta,\Lambda$ そのものがカットのない導出 $E$ をもつ。$D$ のこのカットで終わる部分を $E$ に取り替えても、下の規則の前提と結論は変わらないので、固有変数の条件を含めて $D$ の残りはそのまま正しい。カットの個数は 1 減ったので、帰納法の仮定により結論を得る。証明の各段は導出を具体的に作っているので、手続きは計算可能である。$\square$