シーケント計算とカット除去

証明論の主定理 — 近道を消しても結論は変わらない

このページの目標

シーケント $\Gamma \vdash \Delta$ の読み方と、左規則・右規則による証明の組み立てを理解する。カット規則（補題の利用）と、それを消せるというカット除去定理、その帰結である部分論理式性と無矛盾性をつかむ。

1. シーケントとは

シーケントは $\Gamma \vdash \Delta$ という形をしている。$\Gamma$（前件）と $\Delta$（後件）はどちらも論理式の並びである。読み方はこうである。

$A_1, \dots, A_m \vdash B_1, \dots, B_n$ は、「$A_1$ かつ … かつ $A_m$ がすべて成り立つなら、$B_1$ または … または $B_n$ の少なくとも一つが成り立つ」と読む。つまり左辺は連言、右辺は選言として効く。古典論理では、これは $\Gamma \vdash \Delta$ を $(\bigwedge \Gamma) \to (\bigvee \Delta)$ と読むことに対応する。

自然演繹（初級）が「一つの結論」を導く縦の証明木だったのに対し、シーケント計算は仮定と結論の集まりの関係を一行で扱う。各結合子には、その結合子が左辺に現れる場合（左規則）と右辺に現れる場合（右規則）の規則を与える。

規則の例（連言と含意）

出発点は公理 $A \vdash A$（同じ式は自分から導ける）。そこから下向きに組み立てる。

$$A \vdash A \quad(\text{公理}) \qquad \dfrac{\Gamma \vdash \Delta,\, A \quad \Gamma \vdash \Delta,\, B}{\Gamma \vdash \Delta,\, A \land B}\ (\land\text{R})$$ $$\dfrac{\Gamma \vdash \Delta,\, A \quad \Gamma,\, B \vdash \Delta}{\Gamma,\, A \to B \vdash \Delta}\ (\to\text{L})$$

$(\land\text{R})$ は「右辺に $A \land B$ を作るには、$A$ と $B$ を別々に示せばよい」。$(\to\text{L})$ は「左辺に $A \to B$ がある（使える）とき、$A$ を示し、$B$ を仮定して先へ進む」と読む。各結合子に左右の規則がそろう。

このほかに、論理式を増やしたり重複を縮めたり順序を入れ替えたりする構造規則（弱化・縮約・交換）がある。これらは「使う材料の個数や順番」を整える補助的な規則である。

2. カット規則 — 補題を使う

数学の証明では、いったん補題 $A$ を証明し、それを道具にして本題を進めることが多い。これを規則にしたのがカット (cut) である。

カット規則
$$\dfrac{\Gamma \vdash \Delta,\, A \qquad A,\, \Gamma \vdash \Delta}{\Gamma \vdash \Delta}\ (\text{Cut})$$

左の枝で補題 $A$ を結論として示し、右の枝でその $A$ を仮定として使う。結果として $A$ は最終結論から消える（＝カットされる）。「$A$ を経由して進む」という、ごく自然な推論である。（ここでは両枝の文脈をそろえて $\Gamma, \Delta$ と書いたが、一般には左右の枝の文脈は独立で、$\Gamma \vdash \Delta,\, A$ と $A,\, \Pi \vdash \Lambda$ から $\Gamma,\, \Pi \vdash \Delta,\, \Lambda$ を導く形が標準である。）

カットは便利で、証明を短く・読みやすくする。一方で、カットされる補題 $A$ は最終結論のどこにも現れない。証明の途中に「結論と無関係な式」が現れうる、ということである。これが後で効いてくる。

3. カット除去定理（Gentzen の基本定理）

Gentzen が示したカット除去定理（Hauptsatz、1934-35）は、次のように述べる。

定理（カット除去）：カット規則を使うどんな証明も、カットをまったく使わない証明に変換できる。

言いかえれば、補題という「近道」は原理的には不要で、すべて展開してカットフリーの証明にできる。変換は機械的な手続きで、カットを上へ押し上げては小さく分解していく（その過程で証明は爆発的に大きくなりうるが、必ず終わる）。

カットあり ⊢ A A ⊢ (Cut) Γ ⊢ Δ 補題 A は結論に無い 変換 カット除去後（カットフリー） 部分論理式だけ Γ ⊢ Δ
図 1: カット除去の模式図。左はカット規則で補題 $A$ を経由する証明だが、$A$ は結論 $\Gamma \vdash \Delta$ に現れない。右はカットを除去した証明で、現れる論理式はすべて結論の部分論理式になる。証明は大きくなりうるが、結論は変わらない。
図 1 の内容をテキストで読む

左の証明は、補題 $A$ を結論として示す枝（$\vdash A$）と、$A$ を仮定として使う枝（$A \vdash$）をカット規則で結び、結論 $\Gamma \vdash \Delta$ を得る。補題 $A$ は最終結論に現れない。右はカット除去後の証明で、カットが消え、証明に現れる論理式はすべて結論の部分論理式になっている。結論は同じだが、証明の形（とサイズ）が変わる。

4. 部分論理式性とその帰結

カットフリーの証明には、際立った性質がある。

部分論理式性：カットフリーの証明に現れる論理式は、すべて結論（最下段のシーケント）の部分論理式である。

証明の途中に、結論と無関係な式は一切現れない。各規則を下から上へ見ると、結合子を一つずつ外すだけだからである。ここから重要な帰結が得られる。

  • 無矛盾性：空のシーケント $\vdash$（「何の仮定もなく矛盾」）には、カットフリーの証明が存在しない（最下段に論理式がないので、適用できる規則がない）。カット除去により、矛盾を導くカット付き証明も存在しないと分かる。これが（命題論理・一階述語論理の）無矛盾性の証明論的な根拠になる。ただし算術の無矛盾性はこれだけからは従わず、Gentzen はのちに $\varepsilon_0$ までの超限帰納法を用いて別途証明した。
  • 証明探索：現れる式が部分論理式に限られるので、結論から上へ機械的に証明を探索できる。命題論理ではこれが決定手続きを与える（計算可能性・決定可能性と接続する）。
  • 正規化との対応：自然演繹側では、カット除去は証明の正規化に対応する。Curry–Howard のもとで、これは型付き項の簡約が停止すること（強正規化）と表裏一体である。

まとめ

この章のポイント

  • シーケント $\Gamma \vdash \Delta$：左辺は連言、右辺は選言として効く
  • 各結合子に左規則・右規則を与え、構造規則（弱化・縮約・交換）で材料を整える
  • カット＝補題の利用。補題は最終結論に現れない
  • カット除去定理（Gentzen）：カットはすべて消せる。結論は変わらないが証明は大きくなりうる
  • 部分論理式性から、無矛盾性・証明探索（決定手続き）・正規化との対応が導かれる

よくある質問

シーケント計算とは何か

Gentzen が導入した証明体系で、$\Gamma \vdash \Delta$ というシーケントを扱う。左辺 $\Gamma$ がすべて成り立てば右辺 $\Delta$ の少なくとも一つが成り立つ、という意味である。各結合子に左規則と右規則を与え、結論から上へ論理式を分解していく形で証明を構成する。

カット除去定理とは何か

カット規則は「補題 $A$ をいったん証明し、それを使って先へ進む」推論である。カット除去定理（Gentzen の基本定理）は、カットを使う証明はすべてカットを使わない証明に変換できる、と述べる。補題という近道を消しても結論は変わらない、という主張である。

部分論理式性がなぜ重要なのか

カットフリーの証明では、現れる論理式がすべて結論の部分論理式になる。証明の途中に無関係な式が現れないため、証明を下から機械的に探索でき、また空シーケント $\vdash$ には証明がないと分かる。これが無矛盾性の証明や決定手続きの基礎になる。