ゲンツェンの無矛盾性証明

0. 全体像

ゲンツェン（1936）の主張は次のとおりです。

$\mathrm{PRA} + \mathrm{TI}(\varepsilon_0) \vdash \mathrm{Con}(\mathrm{PA})$

ここで $\mathrm{TI}(\varepsilon_0)$ は、原始再帰的な整列順序 $(\varepsilon_0, <)$ 上の、限量子を含まない式に対する超限帰納法です。

以下で述べるのは、シュッテによる再構成（ω規則を使う無限証明図版）です。ゲンツェン自身の原論文は有限の証明図を書き換える方式で、ω規則は使いません。論理的な骨格は同じなので、見通しの良い版で説明します。

証明の流れを図にします。

 PA で ⊥ が証明できたと仮定(背理法)
        │
        │ ① 埋め込み(帰納法 → ω規則)
        ▼
 ⊢^{ω+m}_{k} ∅       ← 高さ ω+m、カット階数 k
        │
        │ ② カット除去 ×k 回(1回ごとに高さが 2^α へ指数化)
        ▼
 ⊢^{2_k(ω+m)}_{0} ∅  ← カットなし、高さ <ε₀
        │
        │ ③ カットなし証明の構造から
        ▼
       矛盾(空の式は導出できない)

直観を先に述べます。PAの帰納法公理は「無限個の事例を一括して主張するもの」です。ω規則は、その無限個の事例を明示的に並べて、帰納法を「証明の無限の広がり」に変換します。広がりを許す代償として、証明図は無限の高さ（順序数）を持ちます。カット除去は証明を簡単にする操作ですが、1段階ごとに順序数が指数的に膨らみます。PAのカット階数は有界でないため、必要な順序数の上限は $\omega, \omega^\omega, \omega^{\omega^\omega}, \dots$ の極限、すなわち $\varepsilon_0$ になります。

1. 準備：Tait流の体系

1.1 言語と式

言語は $0, S, +, \cdot, =$ と原始再帰的関係です。式は否定標準形で書きます。否定は原子式にだけ付き、 $\wedge, \vee, \forall, \exists$ を使います。式 $A$ の双対を $\neg A$ と書き、ド・モルガンの法則で定義します。

$\neg(A \wedge B) := \neg A \vee \neg B,\quad \neg \forall x A(x) := \exists x \neg A(x)$

式の階数 $\mathrm{rk}(A)$ は、論理記号（ $\wedge, \vee, \forall, \exists$ ）の個数です。原子式とその否定の階数は $0$ です。閉項は値が決まるので、閉原子式は真偽が決定可能です。数字（numeral）を $\bar{n} = S^n 0$ と書きます。

1.2 無限証明体系 $\mathrm{PA}_\omega$

導出可能性を $\vdash^{\alpha}_{k} \Gamma$ と書きます。ここで $\Gamma$ は閉式の有限集合（選言的に読む）、 $\alpha$ は順序数（高さの上界）、 $k$ はカット式の階数の上界です。規則は以下のとおりです。

(Ax)： $\Gamma$ が真な閉原子式（またはその否定）を含むなら $\vdash^{\alpha}_{k} \Gamma$ 。
( $\vee$ )： $\vdash^{\alpha_0}_{k} \Gamma, A_i$ （ $\alpha_0 < \alpha$ 、 $i = 0, 1$ ）から $\vdash^{\alpha}_{k} \Gamma, A_0 \vee A_1$ 。
( $\wedge$ )： $\vdash^{\alpha_0}_{k} \Gamma, A_0$ と $\vdash^{\alpha_1}_{k} \Gamma, A_1$ （ $\alpha_0, \alpha_1 < \alpha$ ）から $\vdash^{\alpha}_{k} \Gamma, A_0 \wedge A_1$ 。
( $\exists$ )： $\vdash^{\alpha_0}_{k} \Gamma, A(\bar{n})$ （ $\alpha_0 < \alpha$ ）から $\vdash^{\alpha}_{k} \Gamma, \exists x A(x)$ 。
( $\omega$ )：すべての $n \in \mathbb{N}$ について $\vdash^{\alpha_n}_{k} \Gamma, A(\bar{n})$ （ $\alpha_n < \alpha$ ）から $\vdash^{\alpha}_{k} \Gamma, \forall x A(x)$ 。
(Cut)： $\vdash^{\alpha_0}_{k} \Gamma, C$ と $\vdash^{\alpha_0}_{k} \Gamma, \neg C$ （ $\alpha_0 < \alpha$ 、 $\mathrm{rk}(C) < k$ ）から $\vdash^{\alpha}_{k} \Gamma$ 。

ω規則は無限個の前提を持つので、証明図は無限分岐の整礎木になります。高さに順序数が現れるのはこのためです。

2. ステップ①：PAからの埋め込み

補題1（埋め込み） $\mathrm{PA} \vdash \Gamma(x_1, \dots, x_l)$ ならば、ある $m, k < \omega$ が存在して、任意の数字 $\bar{n}_1, \dots, \bar{n}_l$ について次が成り立つ。

$\vdash^{\omega + m}_{k} \Gamma(\bar{n}_1, \dots, \bar{n}_l)$

証明の要点。 PAの証明図の長さに関する帰納法で示します。

論理公理 $\neg A, A$ は、 $A$ の構成に関する帰納法で、有限の高さ（ $\le 2\,\mathrm{rk}(A)$ ）・カットなしで導出できます。
PAの非論理公理は閉じた事例が真なので、(Ax) で処理できます。
推論規則のうち、論理規則は対応する規則で処理できます。カットは(Cut)にそのまま対応します。
帰納法公理が核心です。帰納法公理の事例を Tait 形式で書くと次のとおりです。

$\neg A(0),\ \exists x\,(A(x) \wedge \neg A(Sx)),\ \forall x A(x)$

( $\omega$ ) により、各 $n$ について次を示せば十分です。

$\neg A(0),\ \exists x\,(A(x) \wedge \neg A(Sx)),\ A(\bar{n})$

これは $n$ に関する通常の帰納法で、カットなしで導出できます。

$n = 0$ ：論理公理です。
$n \to n+1$ ：記号を簡単にするため $\Gamma' := \{\neg A(0),\ \exists x(A(x) \wedge \neg A(Sx)),\ A(\overline{n+1})\}$ とおきます。帰納法の仮定（弱化したもの）から $\vdash \Gamma', A(\bar{n})$ が得られます。一方、 $\Gamma'$ は $A(\overline{n+1})$ を含むので、 $\vdash \Gamma', \neg A(\overline{n+1})$ は論理公理です。この2つに ( $\wedge$ ) を適用して $\Gamma', A(\bar{n}) \wedge \neg A(\overline{n+1})$ を得ます。さらに ( $\exists$ )（証人 $\bar{n}$ ）を適用すると $\exists x(\ldots)$ が得られ、これは $\Gamma'$ にすでに含まれています。

各 $n$ での導出の高さは有限（ $<\omega$ ）なので、( $\omega$ ) の適用により、帰納法公理は 高さ $\omega$ 、カット階数 $0$ で導出できます。

あとはPA証明図の残りの推論の個数 $m$ （有限）だけ高さが増えます。カット階数 $k$ は、元の証明図に現れるカット式の階数の最大値で、これも有限です。 ∎

ここがポイント。 帰納法という「有限的な対象についての無限的な主張」が、ω規則によって高さ $\omega$ の証明図に翻訳されました。この時点で順序数 $\omega$ が登場します。

3. ステップ②：カット除去

3.1 補助補題（逆転）

補題2（逆転） 次が成り立つ。

$\vdash^{\alpha}_{k} \Gamma, A_0 \wedge A_1$ ならば $\vdash^{\alpha}_{k} \Gamma, A_i$ （ $i = 0, 1$ ）。
$\vdash^{\alpha}_{k} \Gamma, \forall x A(x)$ ならば、任意の $n$ について $\vdash^{\alpha}_{k} \Gamma, A(\bar{n})$ 。

高さもカット階数も保存されます。証明は $\alpha$ に関する帰納法で、主論理式が $A_0 \wedge A_1$ （または $\forall x A$ ）である箇所を $A_i$ （または $A(\bar{n})$ ）に置き換えます。

3.2 還元補題

補題3（還元） $\mathrm{rk}(C) = k$ で、 $\vdash^{\alpha}_{k} \Gamma, C$ かつ $\vdash^{\beta}_{k} \Gamma, \neg C$ ならば、次が成り立つ。

$\vdash^{\alpha + \beta}_{k} \Gamma$

証明の核（ $C = \forall x A(x)$ の場合）。 $\alpha + \beta$ に関する帰納法で示します。双対 $\neg C = \exists x \neg A(x)$ が右の導出の最後の規則で主論理式になっている場合を考えます。このとき右の前提は次の形です。

$\vdash^{\beta_0}_{k} \Gamma, \neg C, \neg A(\bar{m}) \quad (\beta_0 < \beta)$

帰納法の仮定を、左全体 $(\Gamma, C)$ と、右の前提 $(\Gamma, \neg C, \neg A(\bar{m}))$ に適用します。すると $\vdash^{\alpha + \beta_0}_{k} \Gamma, \neg A(\bar{m})$ が得られます。
補題2（逆転）を左に適用します。すると $\vdash^{\alpha}_{k} \Gamma, A(\bar{m})$ が得られます。
この2つに カット式 $A(\bar{m})$ でカットします。 $\mathrm{rk}(A(\bar{m})) = k - 1 < k$ なので、カット階数は $k$ のままです。高さは $\max(\alpha, \alpha + \beta_0) + 1 \le \alpha + \beta$ です。

他の場合も同様の計算です。 ∎

図で表すと次のとおりです。

   ∀xA(x) をカット式とするカット(階数 k)
                    ↓ 還元
   A(m̄) をカット式とするカット(階数 k-1)

これが「カットの複雑さを1段下げる」ための基本操作です。

3.3 1段階のカット除去

補題4（カット除去・1段階）

$\vdash^{\alpha}_{k+1} \Gamma \ \Longrightarrow\ \vdash^{2^{\alpha}}_{k} \Gamma$

証明。 $\alpha$ に関する帰納法で示します。

最後の規則が(Cut)でないか、カット式の階数が $k$ 未満の場合は、前提に帰納法の仮定を適用して同じ規則を適用します。高さは $2^{\alpha_i} < 2^{\alpha}$ です。
最後の規則が階数ちょうど $k$ のカット式 $C$ に対するカットの場合、前提 $\vdash^{\alpha_0}_{k+1} \Gamma, C$ と $\vdash^{\alpha_0}_{k+1} \Gamma, \neg C$ に帰納法の仮定を適用して、 $\vdash^{2^{\alpha_0}}_{k} \Gamma, C$ と $\vdash^{2^{\alpha_0}}_{k} \Gamma, \neg C$ を得ます。補題3を適用すると、高さ $2^{\alpha_0} + 2^{\alpha_0} = 2^{\alpha_0 + 1} \le 2^{\alpha}$ で $\Gamma$ が得られます。 ∎

3.4 繰り返し

指数塔を次のように定義します。

$2_0(\alpha) := \alpha,\qquad 2_{k+1}(\alpha) := 2^{2_k(\alpha)}$

補題4を $k$ 回繰り返すと次が得られます。

系5（カット完全除去）

$\vdash^{\alpha}_{k} \Gamma \ \Longrightarrow\ \vdash^{2_k(\alpha)}_{0} \Gamma$

4. ステップ③：矛盾の導出

PAが矛盾する、すなわち空式 $\emptyset$ が証明できたと仮定します。

補題1より $\vdash^{\omega + m}_{k} \emptyset$ 。
系5より $\vdash^{2_k(\omega + m)}_{0} \emptyset$ 。

カットなしの証明図で空式が導出されることはありません。 理由は次のとおりです。導出の最後の規則を見ます。(Ax) は結論に真な原子式が必要です。他の規則はすべて結論に主論理式が必要です。空式にはどちらもありません。

これは矛盾なので、PAは無矛盾です。 ∎

5. なぜ $\varepsilon_0$ なのか

$2_k(\omega + m)$ は、どんな $k, m < \omega$ についても $\varepsilon_0$ 未満です。ここで

$\varepsilon_0 := \sup\{\omega,\ \omega^{\omega},\ \omega^{\omega^{\omega}},\ \dots\}$

は $\omega^{\varepsilon_0} = \varepsilon_0$ を満たす最小の順序数です。

PAのカット階数は有界でない（ $k$ はPAの証明ごとに異なり、いくらでも大きくなる）ので、必要な順序数の上限は各 $k$ ごとの指数塔の上限になります。1段階のカット除去で指数が1段積み上がるので、その上限が $\varepsilon_0$ です。

 順序数の階段
 ω  <  ω^ω  <  ω^(ω^ω)  <  ...  →  ε₀
 ↑       ↑         ↑
 k=0     k=1       k=2    (カット階数 k が大きいほど、除去後に必要な高さも大きい)

6. 形式化とゲーデルの第二不完全性定理との関係

ここまでの議論は、ω規則を持つ無限的体系を用いているので、そのままでは有限の立場で行ったことになりません。形式化は次のように行います。

無限証明図を、再帰的な木のコードとして算術化します。
カット除去の操作を原始再帰的な操作として定義します。
結論「カットなし導出に到達する」を、順序数 $<\varepsilon_0$ に関する超限帰納法で示します。

その結果、 $\mathrm{PRA} + \mathrm{TI}(\varepsilon_0) \vdash \mathrm{Con}(\mathrm{PA})$ が得られます。ここで使う $\mathrm{TI}(\varepsilon_0)$ は、原始再帰的な述語に対するものです。

6.1 ゲーデルの第二不完全性定理と矛盾しない理由

第二不完全性定理は $\mathrm{PA} \nvdash \mathrm{Con}(\mathrm{PA})$ を主張します。ゲンツェンの結果と合わせると、次が導かれます。

$\mathrm{PA} \nvdash \mathrm{TI}(\varepsilon_0)$

もしPAが $\mathrm{TI}(\varepsilon_0)$ を証明できたら、 $\mathrm{PRA} \subset \mathrm{PA}$ ですから、PAは自身の無矛盾性を証明してしまい、第二不完全性定理に反するからです。

6.2 各 $\alpha < \varepsilon_0$ については証明できる

ゲンツェンは、 $\mathrm{PA} \vdash \mathrm{TI}(\alpha)$ が各 $\alpha < \varepsilon_0$ について成り立つことも示しました。これで $\varepsilon_0$ が「ちょうどの強さ」であることが分かります。証明の鍵はジャンプ補題です。

$\mathrm{Prog}(F) := \forall x\,(\forall y < x\ F(y) \to F(x))$ と定義します。
式 $F$ に対し、 $F^{+}(x) := \forall y\,(\forall z < y\ F(z) \to \forall z < y + \omega^{x}\ F(z))$ を定義します。

このとき次が成り立ちます。

$\mathrm{Prog}(F) \to \mathrm{Prog}(F^{+})$

したがって $\mathrm{TI}(\alpha + 1, F^{+})$ から $\mathrm{TI}(\omega^{\alpha}, F)$ が出ます。これを繰り返すと、各 $n$ について $\mathrm{TI}(\omega_n)$ が証明されます（ここで $\omega_0 = 1,\ \omega_{n+1} = \omega^{\omega_n}$ ）。

ただし $F \mapsto F^{+}$ は式の複雑さを上げるので、PAは各 $n$ ごとに証明できるだけで、すべての $n$ を一様に扱うことはできません。ここが $\varepsilon_0$ との境目になります。

7. まとめ

段階	内容	順序数の動き
① 埋め込み	帰納法 → ω規則	$\omega + m$ が登場
② カット除去	階数 $k$ を $0$ へ	$2_k(\omega + m)$ まで増加
③ 矛盾	カットなしでは空式は導出不能	$<\varepsilon_0$

要点は3つです。

PAの強さは $\varepsilon_0$ で測られる。 順序数解析におけるPAの証明論的順序数は $\varepsilon_0$ です。
有限の立場に収まらないのは $\mathrm{TI}(\varepsilon_0)$ だけ。 無矛盾性の証明に必要な「新しい原理」を、超限帰納法という1点に押し込めたのがゲンツェンの貢献です。
算術的な帰結もある。 $\varepsilon_0$ に結びつくグッドスタインの定理は、PAでは証明できません（Kirby–Paris）。ゲンツェンの結果と同じ現象を、別の形で見たものです。

必要であれば、次の話題も詳しく扱えます。

原論文の有限的な証明図書き換え（end-piece、還元ステップ、順序数割り当て）の詳細
ジャンプ補題の証明の完全版
$\mathrm{TI}(\varepsilon_0)$ の $\mathrm{PRA}$ 内での形式化の詳細

ヒドラゲームとゲンツェンの証明の対応

0. 先に結論

両者は、順序数 $<\varepsilon_0$ の降下という同じ骨格を共有しています。ヒドラゲームは、ゲンツェンの証明のうち「順序数の割り当て・還元で順序数が減る・ $\varepsilon_0$ の整礎性は PA で証明できない」という部分を、純粋に組合せ論的な形で取り出した「ミニチュア」です。

ヒドラゲーム	順序数側	ゲンツェンの証明側
ヒドラ（有限根付き木） $T$	$o(T) < \varepsilon_0$	証明図に付けた順序数（高さ $\alpha$ ）。「残りの複雑さの見積り」
ルール：頭を切る	$\alpha \to \alpha' < \alpha$	還元（証明図の簡約）1ステップ
展開：根でない頭を切ると、時刻 $n$ に応じて部分木が $n$ 個再生	$\omega^{\beta'+1} \to \omega^{\beta'+1}[n+1]$ （基本列の $(n+1)$ 番目）	ω規則の $n$ 番目の前提を取る／帰納法を $n$ 回に展開する／部分証明を複製する
Hercules の戦略は任意	降下の経路は任意	簡約するレデックスの選び方は任意（強正規化）
ゲームは必ず終わる	$\varepsilon_0$ の整礎性	カット除去が停止する（ $\mathrm{TI}(\varepsilon_0)$ の使用）
終わるまでの長さが天文学的	Hardy 関数 $H_\alpha$	カット除去の高さ爆発 $2_k(\cdot)$

この対応は厳密な同型ではなく、順序数を媒介にした構造的な対応です。ヒドラは証明図そのものを符号化しているわけではありません。以下、順に説明します。

1. ヒドラゲームのルールと展開

1.1 ルール

ヒドラは有限の根付き木です。葉が「頭」、根が「胴体」にあたります。時刻 $n = 1, 2, 3, \dots$ に、Hercules は次の手を打ちます。

頭（葉） $h$ を1つ選んで切る。その親を $r$ とする。
$r$ が根の場合：何も起こらない（頭が1つ減るだけ）。
$r$ が根でない場合： $r$ の親を $s$ とする。頭 $h$ を除いたあとの $r$ を根とする部分木を $T_r'$ とする。 $s$ に、 $T_r'$ のコピーを $n$ 個追加する（結果として $s$ の下には $T_r'$ が $n+1$ 個並ぶ）。

定理（Kirby–Paris） Hercules はどんな戦略でも必ず勝つ（有限回で頭が全部なくなる）。ただしこの定理は PA では証明できない。

1.2 具体例

初期状態は、根 $R$ の下に $r$ があり、 $r$ が葉を2つ持つ木です。

 [初期]            [n=1: 左の頭を切る]      [n=2: 左の r の頭を切る]
    R                     R                       R
    |                    / \                  / | \  \
    r                   r   r                •  •  •  r
   / \                  |   |                           |
  •   •                 •   •                           •
  o = ω²             o = ω·2                  o = ω + 3

$n = 1$ ： $r$ の左の頭を切ります。 $r$ が頭を1つ失い、 $s = R$ に $T_r'$ の複製が1個追加されます。
$n = 2$ ：左の $r$ の頭を切ります。この $r$ は葉になり、 $R$ に葉のコピーが2個追加されます（合計で葉3つ）。

頭の数は増えていますが、ゲームは終わります。理由は次節の順序数で説明します。

2. ヒドラへの順序数の割り当て

2.1 Cantor 標準形との対応

木 $T$ に順序数 $o(T)$ を再帰的に割り当てます。

葉： $o = 0$ （空和）。
根の子の部分木が $T_1, \dots, T_k$ であるとき：

$o(T) := \omega^{o(T_1)} + \cdots + \omega^{o(T_k)} \quad (o(T_1) \ge \cdots \ge o(T_k))$

これは $\varepsilon_0$ 未満の順序数の Cantor 標準形そのものです。同型を除く有限根付き木 と $\varepsilon_0$ 未満の順序数 は、この割り当てで一対一に対応します。

2.2 頭を切ると順序数が減る

(a) 根の頭を切る場合。 項 $\omega^0 = 1$ が1つ消えるので、順序数は $\alpha + 1 \to \alpha$ と減ります。

(b) 根でない頭を切る場合。 親 $r$ は葉の子を持つので、部分木の順序数は後者順序数になります。 $o(T_r) = \beta' + 1$ とおくと、頭を切ったあとの $T_r'$ の順序数は $\beta'$ です。 $s$ の側では、項 $\omega^{\beta'+1}$ が $(n+1)$ 個の $\omega^{\beta'}$ に置き換わります。

$\omega^{\beta'+1} \ \longrightarrow\ \underbrace{\omega^{\beta'} + \cdots + \omega^{\beta'}}_{n+1} = \omega^{\beta'} \cdot (n+1)$

$\omega^{\beta'} \cdot (n+1) < \omega^{\beta'} \cdot \omega = \omega^{\beta'+1}$ なので、 $s$ の部分木の順序数は真に減ります。標準形（自然和）は各引数について狭義単調なので、木全体の順序数も真に減ります。

$\varepsilon_0$ 未満の順序数に無限降下列は存在しないので、ゲームは有限回で終わります。この証明で使っているのが $\varepsilon_0$ 上の超限帰納法 $\mathrm{TI}(\varepsilon_0)$ です。

2.3 展開 = 基本列の取り出し

(b) の置き換え $\omega^{\beta'+1} \to \omega^{\beta'} \cdot (n+1)$ は、極限順序数 $\omega^{\beta'+1}$ の基本列（ $\lambda$ に近づく列）の $(n+1)$ 番目の元を取ることです。

$\omega^{\beta'+1}[n] := \omega^{\beta'} \cdot n$

ヒドラの1手は、次のように言い換えられます。

根の頭を切る：後者から前者へ $\alpha + 1 \to \alpha$ 。
根でない頭を切る：ある極限項 $\lambda$ を $\lambda[n+1]$ に置き換える。

つまり、ヒドラゲームは「基本列に沿った順序数の降下」を、木の形で見えるようにしたものです。時刻 $n$ はその基本列のインデックスにあたります。

3. ゲンツェンの証明との対応

先に書いたシュッテ流の再構成（ $\mathrm{PA}_\omega$ ）と対応づけます。

3.1 順序数割り当て：木 ↔ 順序数 ↔ 導出の高さ

ゲンツェンは、PA における $\bot$ （空式）の証明に順序数を割り当て、還元のたびに順序数が減ることを示します。 $\mathrm{PA}_\omega$ 版では、導出の高さ $\alpha$ がこの順序数にあたります。ヒドラの $o(T)$ も同じ役割（降下の進行度を測る量）を担っています。

3.2 頭を切る ↔ 還元の1ステップ

根の頭を切る場合（複製なし）。 $\alpha + 1 \to \alpha$ は、有限の規則（ $\wedge, \vee, \exists$ 、Cut）で導出の直前の前提に降りることに対応します。

根でない頭を切る場合（複製あり）。 これが興味深い部分で、 $\omega^{\beta'+1}$ は $\omega^{\beta'} \cdot \omega$ と書けます。「 $\omega^{\beta'}$ ステップの塊を、ω 回（無限回）繰り返す」という形です。この「無限回の繰り返し」を具体的な有限回 $n+1$ に置き換えるのが展開です。ゲンツェン側で、これに対応する場面は3つあります。

帰納法の展開。 2節の埋め込みで見たとおり、帰納法はω規則に翻訳され、高さ $\omega$ を持ちます。帰納法の項が数字 $\bar{n}$ に評価されたとき、前提の導出を $n$ 回複製してカットでつなぐ形に展開されます。これはヒドラの「部分木を $n$ 個複製する」操作と同型の構造です。ゲンツェン原論文の有限版では、帰納法推論の順序数は概略として「前提の順序数 $\times\ \omega$ 」型の値を持ち、展開すると「前提の順序数 $\times\ n$ 」型の値に下がります。これは $\omega^{\beta'} \cdot \omega \to \omega^{\beta'} \cdot n$ と同じ形です（細部は定式化によって異なるので、構造の対応として理解してください）。
ω規則の $m$ 番目の前提を取る。 還元補題（補題3）の核心では、∀ のカットを $A(\bar{m})$ のカットに還元しました。このとき、無限個の前提のうち $m$ 番目を選んでいます。これも「基本列の1つの元を取る」操作です。
部分証明の複製。 補題3の証明では、左の導出 $\vdash^{\alpha}_{k} \Gamma, C$ が2回使われました（帰納法の仮定の適用と、逆転補題の適用）。1つの部分証明が複数コピーされるという点がヒドラの再生と同じです。複製のたびに、より単純な（階数 $k-1$ の）カットに置き換わるので、全体の順序数は減ります。

3.3 戦略が任意 ↔ 強正規化

Hercules はどの頭を切ってもよく、どの戦略でもゲームは終わります。ゲンツェンの還元も同様で、簡約できる箇所（レデックス）が複数あってどれを選んでも停止します。これは強正規化の性質です。

3.4 ゲームの終了 ↔ カット除去の停止 ↔ $\mathrm{TI}(\varepsilon_0)$

ヒドラ： $\varepsilon_0$ の整礎性を使って、ゲームが終わることを証明する。
ゲンツェン： $\varepsilon_0$ の整礎性を使って、カット除去が終わることを証明する。

両者が使っている原理は同じ $\mathrm{TI}(\varepsilon_0)$ です。

3.5 対応の図

 ヒドラの手                          ゲンツェン側(PA_ω)
 ─────────────────────────────────────────────────────────────
 頭を切る(根の直下)            ←→   有限規則で直前の前提へ降りる
 α+1 → α                            

 頭を切る(根でない)            ←→   ω規則の n 番目の前提を取る
 ω^(β'+1) → ω^β'·(n+1)              /帰納法を n 回に展開
                                    /部分証明を複製してカット階数を下げる

 木全体の順序数 o(T) が減る    ←→   導出の高さ/順序数 α が減る

 ゲームが終わる                ←→   カットなし導出に到達する
 (TI(ε₀) を使用)                    (TI(ε₀) を使用)

4. 不可証性の対応

4.1 ヒドラ定理は PA では証明できない

PA は、各 $\alpha < \varepsilon_0$ について「 $o(T) = \alpha$ のヒドラでゲームが終わる」ことを証明できます。これは PA が各 $\mathrm{TI}(\alpha)$ を証明できること（ジャンプ補題）に対応します。しかし、すべてのヒドラについて一様に 終わることは証明できません。これは $\mathrm{PA} \nvdash \mathrm{TI}(\varepsilon_0)$ に対応します。

不可証性の直接の証明は、ゲームの長さの増大度を使います。

ゲームの長さは、Hercules が最右の頭を切る戦略などで、概ね Hardy 関数 $H_{o(T)}(1)$ 程度になります（正確な式は定義の流儀による）。ここで $H_0(x) = x,\ H_{\alpha+1}(x) = H_\alpha(x+1),\ H_\lambda(x) = H_{\lambda[x]}(x)$ です。
Wainer によれば、PA が証明できる全域再帰関数は、ちょうど $H_\alpha$ （ $\alpha < \varepsilon_0$ ）で抑えられる関数です。
したがって「すべてのヒドラで終わる」ことは $H_{\varepsilon_0}$ の全域性を主張しており、PA では証明できません（Cichon）。

4.2 ゲンツェンとの関係

$\mathrm{TI}(\varepsilon_0)$ を認めると PA の無矛盾性が出る（ゲンツェン）ので、ヒドラ定理やグッドスタインの定理は、標準的な基底理論の上で、PA の（1-）無矛盾性に相当する強さを持つことが知られています。つまり「ヒドラが必ず負ける」という一見無害な組合せ論的主張が、PA の無矛盾性より強い主張になっているのです。

5. 対応しない部分

ヒドラは、ゲンツェンの証明のうち順序数の動きの部分を取り出したものです。次の部分はヒドラの中には現れません。

論理的な部分。 PA の証明から $\mathrm{PA}_\omega$ への埋め込み（補題1）、カット除去が実際に可能であること、カットなしの導出では空式が導出できないこと（ステップ③）。
ヒドラの時計 $n$ の由来。 ヒドラでは $n$ は手番の時刻です。ゲンツェンの証明では、これは「ω規則・帰納法・∀ の事例で具体的に選ばれる数字」にあたります。どちらも「基本列のどの元を取るかを、簡約する側が決められない」という点で共通しています。

6. まとめ

ヒドラの木は、 $\varepsilon_0$ 未満の順序数の Cantor 標準形そのものです。
頭を切る手は、基本列に沿った降下 $\alpha \to \alpha'$ です。根でない頭を切って複製が生じるのは、極限項 $\omega^{\beta'+1}$ を基本列の $(n+1)$ 番目に置き換えることです。これは、ゲンツェン側のω規則・帰納法の展開・部分証明の複製に対応します。
ゲームが終わる証明とカット除去が停止する証明は、どちらも $\mathrm{TI}(\varepsilon_0)$ を使います。
$\mathrm{TI}(\varepsilon_0)$ が PA で証明できないことが、ヒドラ定理の PA における独立性と、ゲーデルの第二不完全性定理の下でのゲンツェンの結果の両方を説明します。

HODGE'S PARROT

はてなダイアリーから移行しました。まだ未整理中。

Claude | ゲンツェンの無矛盾性証明とヒドラゲーム

ゲンツェンの無矛盾性証明

0. 全体像

1. 準備：Tait流の体系

1.1 言語と式

1.2 無限証明体系 $\mathrm{PA}_\omega$

2. ステップ①：PAからの埋め込み

3. ステップ②：カット除去

3.1 補助補題（逆転）

3.2 還元補題

3.3 1段階のカット除去

3.4 繰り返し

4. ステップ③：矛盾の導出

5. なぜ $\varepsilon_0$ なのか

6. 形式化とゲーデルの第二不完全性定理との関係

6.1 ゲーデルの第二不完全性定理と矛盾しない理由

6.2 各 $\alpha < \varepsilon_0$ については証明できる

7. まとめ

ヒドラゲームとゲンツェンの証明の対応

0. 先に結論

1. ヒドラゲームのルールと展開

1.1 ルール

1.2 具体例

2. ヒドラへの順序数の割り当て

2.1 Cantor 標準形との対応

2.2 頭を切ると順序数が減る

2.3 展開 = 基本列の取り出し

3. ゲンツェンの証明との対応

3.1 順序数割り当て：木 ↔ 順序数 ↔ 導出の高さ

3.2 頭を切る ↔ 還元の1ステップ

3.3 戦略が任意 ↔ 強正規化

3.4 ゲームの終了 ↔ カット除去の停止 ↔ $\mathrm{TI}(\varepsilon_0)$

3.5 対応の図

4. 不可証性の対応

4.1 ヒドラ定理は PA では証明できない

4.2 ゲンツェンとの関係

5. 対応しない部分

6. まとめ

ゲンツェンの無矛盾性証明

0. 全体像

1. 準備：Tait流の体系

1.1 言語と式

1.2 無限証明体系

2. ステップ①：PAからの埋め込み

3. ステップ②：カット除去

3.1 補助補題（逆転）

3.2 還元補題

3.3 1段階のカット除去

3.4 繰り返し

4. ステップ③：矛盾の導出

5. なぜ なのか

6. 形式化とゲーデルの第二不完全性定理との関係

6.1 ゲーデルの第二不完全性定理と矛盾しない理由

6.2 各 については証明できる

7. まとめ

ヒドラゲームとゲンツェンの証明の対応

0. 先に結論

1. ヒドラゲームのルールと展開

1.1 ルール

1.2 具体例

2. ヒドラへの順序数の割り当て

2.1 Cantor 標準形との対応

2.2 頭を切ると順序数が減る

2.3 展開 = 基本列の取り出し

3. ゲンツェンの証明との対応

3.1 順序数割り当て：木 ↔ 順序数 ↔ 導出の高さ

3.2 頭を切る ↔ 還元の1ステップ

3.3 戦略が任意 ↔ 強正規化

3.4 ゲームの終了 ↔ カット除去の停止 ↔

3.5 対応の図

4. 不可証性の対応

4.1 ヒドラ定理は PA では証明できない

4.2 ゲンツェンとの関係

5. 対応しない部分

6. まとめ

1.2 無限証明体系 $\mathrm{PA}_\omega$

5. なぜ $\varepsilon_0$ なのか

6.2 各 $\alpha < \varepsilon_0$ については証明できる

3.4 ゲームの終了 ↔ カット除去の停止 ↔ $\mathrm{TI}(\varepsilon_0)$