Gentzenの無矛盾性証明
概要
Gentzenの無矛盾性証明（Gentzen's consistency proof）とは、Peano算術 $\mathsf{PA}$ の無矛盾性を、有限的な推論と、初等的に計算可能な述語についての順序数 $\varepsilon_0$ までの超限帰納法から導く証明である。Schütte の形では、$\mathsf{PA}$ の証明を $\omega$ 規則をもつ無限の導出に埋め込み、カットの階数を 1 下げるごとに高さを $\omega^\alpha$ に上げてカットを除き、高さ $\varepsilon_0$ 未満のカットのない導出を得る。空の列にはカットのない導出がないので無矛盾性が従い、同じ解析から、解釈をもたない述語についての超限帰納法は順序型 $\varepsilon_0$ 以上の順序に沿っては証明できないことも分かる。
Gentzen の無矛盾性証明（Gentzen's consistency proof）は、Gentzen が 1936 年に与えた Peano算術 $\mathsf{PA}$ の無矛盾性の証明である。Gentzen は、有限的に正当化される推論に、初等的に計算可能な述語についての順序数 $\varepsilon_0$ までの超限帰納法を加えれば $\mathsf{PA}$ の無矛盾性が証明できることを示し、さらに $\mathsf{PA}$ が算術の論理式で書ける述語について $\varepsilon_0$ 未満の各順序数までの超限帰納法を証明することを示した（Rat06 §1.1、pp. 46–47）。Gödelの不完全性定理 の第 2 定理と合わせると、$\varepsilon_0$ がちょうど $\mathsf{PA}$ の強さを測る。
集合論の中では、公理が標準モデルで真なことから無矛盾性はすぐ分かる（無矛盾性 の記事の例「Peano 算術」）。Gentzen の結果の意味は、手段を $\varepsilon_0$ までの超限帰納法に絞れ、$\varepsilon_0$ が縮められないことにある。この記事では Schütte による無限の導出を使う形（Rat06 §1.2、pp. 52–53）で、$\mathsf{PA}$ の証明がカットのない高さ $\varepsilon_0$ 未満の導出に移せること（thm-gcp-main）と、解釈をもたない述語記号 $X$ についての超限帰納法が順序型 $\varepsilon_0$ 以上の順序に沿っては証明できないこと（cor-gcp-ti）を証明する。
塔の上限となる順序数
順序数の和・積・冪は 順序数 の記事の定義「順序数の算術」による。和と積は左について狭義単調、和は右について広義単調である（同記事の例「順序数の和と積の非可換性」の後の段落）。
$\tau_0:=\omega$、$\tau_{n+1}:=\omega^{\tau_n}$ とし、$\varepsilon_0:=\sup_{n<\omega}\tau_n$ と定める。順序数 $\alpha$ と自然数 $k$ について $\omega_0(\alpha):=\alpha$、$\omega_{k+1}(\alpha):=\omega^{\omega_k(\alpha)}$ とおく。
- $\beta<\gamma$ なら $\omega^\beta<\omega^\gamma$ である。
- $\alpha<\varepsilon_0$ なら $\omega^\alpha<\varepsilon_0$ であり、すべての $k$ で $\omega_k(\alpha)<\varepsilon_0$ である。
- $\alpha'<\alpha$ なら $\omega^{\alpha'}\cdot3<\omega^\alpha$ であり、$\alpha_0,\alpha_1<\alpha$ なら $\omega^{\alpha_0}+\omega^{\alpha_1}<\omega^\alpha$ である。
要点：1 は冪の単調性と $\omega^\beta<\omega^\beta\cdot\omega=\omega^{\beta+1}$、2 は $\alpha<\tau_n$ なら $\omega^\alpha<\tau_{n+1}$、3 は $\omega^{\alpha'}\cdot3<\omega^{\alpha'}\cdot\omega$ による。
詳しい証明を開く
1：まず $\beta\le\gamma$ なら $\omega^\beta\le\omega^\gamma$ を $\gamma$ についての超限帰納法で示す。$\gamma=\beta$ は等号である。$\gamma=\delta+1>\beta$ なら $\beta\le\delta$ で $\omega^\gamma=\omega^\delta\cdot\omega\ge\omega^\delta\cdot1\ge\omega^\beta$。$\gamma>\beta$ が極限なら $\omega^\gamma$ は $\omega^\beta$ を含む集合の上限である。$\beta<\gamma$ なら $\beta+1\le\gamma$ で、$\omega^\beta\ge1$ と積の左の狭義単調性から $\omega^\beta<\omega^\beta\cdot\omega=\omega^{\beta+1}\le\omega^\gamma$。
2：$\alpha<\varepsilon_0$ ならある $n$ で $\alpha<\tau_n$ で、1 により $\omega^\alpha<\omega^{\tau_n}=\tau_{n+1}\le\varepsilon_0$。後半は $k$ についての帰納法。
3：1 と積の左の狭義単調性から $\omega^{\alpha'}\cdot3<\omega^{\alpha'}\cdot\omega=\omega^{\alpha'+1}\le\omega^\alpha$。後半は $\gamma:=\max(\alpha_0,\alpha_1)$ について、和の単調性から $\omega^{\alpha_0}+\omega^{\alpha_1}\le\omega^\gamma\cdot2\le\omega^\gamma\cdot3<\omega^\alpha$。$\square$
$\varepsilon_0$ は $\omega^\varepsilon=\varepsilon$ を満たす最小の順序数でもある。$\varepsilon_0$ 未満の順序数は Cantor の標準形で自然数に符号化でき、大小は初等的に計算できる（Rat06 p. 47、Theorem 1.4 と続く段落 pp. 48–49。この記事では証明しない）。とくに $\mathbb N$ の上に順序型 $\varepsilon_0$ の整列順序がある。
無限の導出の体系
算術の言語 $\{0,S,+,\cdot,=,<\}$ に 2 項の関係記号 $\prec$ と 1 項の関係記号 $X$ を加えた言語を $L$ とする。$=$ も論理記号でない関係記号として扱う。$\prec$ には $\mathbb N$ の上の 2 項関係を 1 つ固定して解釈として与え、こうして得た構造を $\mathfrak N$ と書く。$X$ には解釈を与えない。閉項 $t$ の値を $t^{\mathfrak N}$、自然数 $n$ の数項を $\underline n$ と書く。
原子論理式とその否定を リテラル といい、リテラルから $\land,\lor,\forall,\exists$ で作った論理式を 否定標準形 の論理式という。その 双対 $\sim\!A$ を、$\sim\!P:=\lnot P$、$\sim\!\lnot P:=P$ とし、$\land$ と $\lor$、$\forall$ と $\exists$ を入れ替えて定める（$\sim\sim\!A=A$）。階数 $\operatorname{rk}$ は、リテラルで $0$、$\land,\lor,\forall,\exists$ を 1 つ付けるごとに成分の最大値に $1$ を足して定める。$\operatorname{rk}(\sim\!A)=\operatorname{rk}A$ で、項の代入で階数は変わらない。$X$ の現れない論理式を「$X$ を含まない」、$\lnot X(t)$ の形のリテラルの現れない論理式を「$X$ について正」という。
$\alpha$ を順序数、$k$ を自然数、$\Gamma$ を否定標準形の文の有限集合とする。関係 $\vdash^\alpha_k\Gamma$ を次の条件で閉じた最小の関係とする（$\Gamma,A$ は $\Gamma\cup\{A\}$）。
- (Ax1) $\Gamma$ が $X$ を含まない真のリテラルを含むなら $\vdash^\alpha_k\Gamma$。
- (Ax2) $\Gamma$ が $X(s)$ と $\lnot X(t)$ を含み $s^{\mathfrak N}=t^{\mathfrak N}$ なら $\vdash^\alpha_k\Gamma$。
- ($\land$) $A\land B\in\Gamma$ で、$\alpha_0,\alpha_1<\alpha$ について $\vdash^{\alpha_0}_k\Gamma,A$ かつ $\vdash^{\alpha_1}_k\Gamma,B$ なら $\vdash^\alpha_k\Gamma$。
- ($\lor$) $A_0\lor A_1\in\Gamma$ で、ある $i$ と $\alpha_0<\alpha$ について $\vdash^{\alpha_0}_k\Gamma,A_i$ なら $\vdash^\alpha_k\Gamma$。
- ($\omega$) $\forall x\,A\in\Gamma$ で、すべての $n\in\mathbb N$ について $\alpha_n<\alpha$ と $\vdash^{\alpha_n}_k\Gamma,A(\underline n)$ があれば $\vdash^\alpha_k\Gamma$。
- ($\exists$) $\exists x\,A\in\Gamma$ で、ある $n$ と $\alpha_0<\alpha$ について $\vdash^{\alpha_0}_k\Gamma,A(\underline n)$ なら $\vdash^\alpha_k\Gamma$。
- (Cut) $\operatorname{rk}C< k$ で、$\alpha_0,\alpha_1<\alpha$ について $\vdash^{\alpha_0}_k\Gamma,C$ かつ $\vdash^{\alpha_1}_k\Gamma,\sim\!C$ なら $\vdash^\alpha_k\Gamma$。
$\Gamma$ は「どれかが成り立つ」と読む。$\alpha$ は木の高さ、$k$ はカット論理式 $C$ の階数の上界で、$\vdash^\alpha_0\Gamma$ はカットのない導出を表す。$\land,\lor,\omega,\exists$ で分解される $\Gamma$ の元を 主論理式 という。
($\omega$) のため導出は無限の木になる。これは シークエント計算 を右辺だけにした Tait 流の体系（Bus98 §1.2.14、pp. 16–17）を無限の規則に広げたものである。
- （弱化）$\vdash^\alpha_k\Gamma$、$\alpha\le\beta$、$k\le m$、$\Gamma\subset\Delta$ なら $\vdash^\beta_m\Delta$。
- （項の取り替え）$s^{\mathfrak N}=t^{\mathfrak N}$ で $A_i(x)$ の自由変数が高々 $x$ なら、$\vdash^\alpha_k\Gamma,A_1(s),\dots,A_j(s)$ から $\vdash^\alpha_k\Gamma,A_1(t),\dots,A_j(t)$ が従う。
- （偽のリテラルの除去）$\ell$ が $X$ を含まない偽の閉じたリテラルなら、$\vdash^\alpha_k\Gamma,\ell$ から $\vdash^\alpha_k\Gamma$ が従う。
- （逆転）$\vdash^\alpha_k\Gamma,A\land B$ なら $\vdash^\alpha_k\Gamma,A$ かつ $\vdash^\alpha_k\Gamma,B$。$\vdash^\alpha_k\Gamma,A\lor B$ なら $\vdash^\alpha_k\Gamma,A,B$。$\vdash^\alpha_k\Gamma,\forall x\,A$ ならすべての $n$ で $\vdash^\alpha_k\Gamma,A(\underline n)$。
どれも $\alpha$ についての超限帰納法で、最後の条件で場合を分ける。
詳しい証明を開く
1：(Ax1)・(Ax2) なら $\Delta$ も同じ条件を満たす。規則なら、前提 $\Gamma,D$ に帰納法の仮定を使って $\vdash^{\alpha_i}_m\Delta,D$ を得て同じ規則を使う（$\alpha_i<\beta$、$\operatorname{rk}C< m$）。
2：閉じた原子論理式の真偽と (Ax2) の判定は項の値だけで決まるので、公理はそのまま公理である。規則の主論理式が $A_i(s)$ なら、前提で加わる論理式 $B(s)$（$\omega,\exists$ では $B(\underline n,s)$）も取り替える一覧に入れて帰納法の仮定を使い、主論理式 $A_i(t)$ で同じ規則を使う。主論理式やカット論理式が $\Gamma$ の側なら、加わる論理式を $\Gamma$ に含めて帰納法の仮定を使う。
3：$\ell$ は (Ax1) の真のリテラルにも (Ax2) の組にも主論理式にもならないので、公理は $\Gamma$ で成り立ち、規則なら前提 $\Gamma,\ell,D$ に帰納法の仮定を使う。
4：$A\land B$ について。公理のリテラルは $\Gamma$ にある。主論理式が $A\land B$ なら、前提 $\Gamma,A\land B,A$（高さ $\alpha_0<\alpha$）に帰納法の仮定を使うと $\vdash^{\alpha_0}_k\Gamma,A$ で、弱化する。ほかの主論理式なら前提に帰納法の仮定を使って同じ規則を使う。$A\lor B$ では前提 $\Gamma,A\lor B,A_i$ から $\Gamma,A,B,A_i=\Gamma,A,B$ を、$\forall x\,A$ では $n$ 番目の前提から $\Gamma,A(\underline n)$ を得る。$\square$
- $A(x)$ の自由変数が高々 $x$ で、閉項 $s,t$ が $s^{\mathfrak N}=t^{\mathfrak N}$ なら、$\vdash^{2\operatorname{rk}A}_0\Gamma,\sim\!A(s),A(t)$。
- $X$ を含まない否定標準形の文 $A$ が $\mathfrak N$ で真なら、$\vdash^{\omega\cdot\operatorname{rk}A}_0\Gamma,A$。
どちらも $\operatorname{rk}A$ についての帰納法である。
詳しい証明を開く
1：リテラルでは、$X$ を含まなければ $\sim\!A(s)$ と $A(t)$ の一方が真なので (Ax1)、$X$ のリテラルなら (Ax2)。$A=B\land C$ なら $\sim\!A(s)=\sim\!B(s)\lor\sim\!C(s)$ で、帰納法の仮定 $\vdash^{2\operatorname{rk}B}_0\Gamma,\sim\!A(s),A(t),\sim\!B(s),B(t)$ に ($\lor$) を使って $\vdash^{2\operatorname{rk}B+1}_0\Gamma,\sim\!A(s),A(t),B(t)$。$C$ も同様にして ($\land$) で高さ $2\operatorname{rk}A$。$A=\forall y\,B(x,y)$ なら、各 $n$ の帰納法の仮定（論理式 $B(x,\underline n)$）に ($\exists$) を使ってから ($\omega$)。$\lor,\exists$ は双対である。
2：真のリテラルは (Ax1)。$A\land B$、$\forall x\,B$ が真なら成分・代入例はすべて真、$A\lor B$、$\exists x\,B$ が真ならある成分・代入例が真である。それらの階数は $\operatorname{rk}A-1$ 以下なので、帰納法の仮定の高さ $\omega\cdot(\operatorname{rk}A-1)$ に規則を 1 回使えば $\omega\cdot\operatorname{rk}A$ 以下になる。$\square$
2 により、真な $X$ を含まない文はカットなしで導出できる。高さが意味をもつのは $X$ を含む列である。
カット除去
$C$ と $\sim\!C$ の一方は、リテラルか、$\lor$ か $\exists$ で始まる。その側を、相手側の逆転で崩していく。
$C$ を、リテラルか $A\lor B$ か $\exists x\,A$ の形の文で $\operatorname{rk}C=k$ のものとする。$\vdash^\alpha_k\Gamma,\sim\!C$ かつ $\vdash^\beta_k\Delta,C$ なら $\vdash^{\alpha+\beta}_k\Gamma,\Delta$ である。
$\vdash^\beta_k\Delta,C$ の最後の条件で分ける。要の場合は $C=A_0\lor A_1$ が主論理式のときである。前提 $\vdash^{\beta_0}_k\Delta,C,A_i$ に帰納法の仮定を使うと $\vdash^{\alpha+\beta_0}_k\Gamma,\Delta,A_i$。$\sim\!C=\sim\!A_0\land\sim\!A_1$ の逆転で $\vdash^\alpha_k\Gamma,\sim\!A_i$。$\operatorname{rk}A_i< k$ なので $A_i$ でカットでき、$\alpha+\beta_0<\alpha+\beta$、$\alpha<\alpha+\beta$（$\beta\ge1$）から $\vdash^{\alpha+\beta}_k\Gamma,\Delta$ を得る。
残りの場合を開く
- $C=\exists x\,A$ が主論理式なら、前提の $A(\underline n)$ と、$\sim\!C=\forall x\,\sim\!A$ の逆転で得る $\sim\!A(\underline n)$ をカットする。
- 公理のリテラルが $\Delta$ にあれば $\Gamma,\Delta$ も公理である。
- (Ax1) の真のリテラルが $C$ なら $\sim\!C$ は偽のリテラルで、lem-gcp-basic の 3 で $\vdash^\alpha_k\Gamma$、弱化する。
- (Ax2) の組の一方が $C$ のとき、$C=X(s)$、$\lnot X(t)\in\Delta$ なら $\vdash^\alpha_k\Gamma,\lnot X(s)$ に lem-gcp-basic の 2 を使って $\vdash^\alpha_k\Gamma,\lnot X(t)$ とし、弱化する。$C=\lnot X(t)$、$X(s)\in\Delta$ も同じ。
- 主論理式かカット論理式が $\Delta$ の側なら、各前提 $\Delta,C,D$（高さ $\beta_i<\beta$）に帰納法の仮定を使って $\vdash^{\alpha+\beta_i}_k\Gamma,\Delta,D$ を得て、同じ規則を使う。
リテラルは主論理式にならないので、場合はこれで尽きる。$\square$
- $\vdash^\alpha_{k+1}\Gamma$ なら $\vdash^{\omega^\alpha}_k\Gamma$ である。
- $\vdash^\alpha_k\Gamma$ なら $\vdash^{\omega_k(\alpha)}_0\Gamma$ である。
1：$\alpha$ についての超限帰納法。公理はそのまま、カット以外の規則と $\operatorname{rk}C< k$ のカットは前提に帰納法の仮定を使って同じ規則を使う（$\omega^{\alpha_i}<\omega^\alpha$、lem-gcp-epsilon の 1）。$\operatorname{rk}C=k$ のカットなら、帰納法の仮定により $\vdash^{\omega^{\alpha_0}}_k\Gamma,C$ と $\vdash^{\omega^{\alpha_1}}_k\Gamma,\sim\!C$ である。$C,\sim\!C$ のうちリテラルか $\lor,\exists$ で始まるほうに lem-gcp-reduction を使うと、高さ $\omega^{\alpha_0}+\omega^{\alpha_1}$ か $\omega^{\alpha_1}+\omega^{\alpha_0}$ で $\Gamma$ が導出でき、lem-gcp-epsilon の 3 によりどちらも $\omega^\alpha$ 未満である。
2：$k$ についての帰納法。$\vdash^\alpha_{k+1}\Gamma$ なら 1 で $\vdash^{\omega^\alpha}_k\Gamma$、帰納法の仮定で $\vdash^{\omega_k(\omega^\alpha)}_0\Gamma$ であり、$\omega_k(\omega^\alpha)=\omega_{k+1}(\alpha)$ は $k$ についての帰納法で分かる。$\square$
階数を 1 下げるたびに高さが $\omega$ の冪に上がる。これが $\varepsilon_0$ の現れる理由である。
主定理：PA の証明をカットのない無限の導出へ移す
導出は シークエント計算 の記事の体系 $\mathbf{LK}$（定義「体系 LK」）を、言語 $L$ に固有変数用の定数記号を無限に加えて使う。$\mathbf{LK}$ の論理式 $A$ の否定標準形 $A^*$ を、原子論理式ではそのまま、$(\lnot A)^*:=\sim\!A^*$、$(A\to B)^*:=\sim\!A^*\lor B^*$ とし、$\land,\lor,\forall,\exists$ とは交換するように定める。$A\leftrightarrow B$ は $(A\to B)\land(B\to A)$ の略記とする。
$L$ の次の文の全体を $\mathsf{PA}(X)$ とする：Peano算術 の記事の定義「Peano算術」の公理 1〜8、等号の公理 (E1) $\forall x\,(x=x)$ と、$L$ の各論理式 $\varphi(x,\vec u)$ についての (E2) $\forall x\forall y\forall\vec u\,\bigl(x=y\to(\varphi(x,\vec u)\to\varphi(y,\vec u))\bigr)$、$L$ の各論理式についての帰納法の公理 $\forall\vec u\,\bigl((\varphi(0,\vec u)\land\forall x\,(\varphi(x,\vec u)\to\varphi(Sx,\vec u)))\to\forall x\,\varphi(x,\vec u)\bigr)$。$\mathfrak N$ で真な $X$ を含まない文の集合 $\mathcal S$ を 1 つとり、$T:=\mathsf{PA}(X)\cup\mathcal S$ とおく。$T$ の有限個の元 $\Gamma_0$ について $\mathbf{LK}\vdash\Gamma_0\Rightarrow\sigma$ となるとき $T\vdash\sigma$ と書き、$\mathbf{LK}\vdash\Gamma_0\Rightarrow$（右辺が空）となるとき $T$ は 矛盾する という。
通常の PA との関係を開く
$\mathcal S=\emptyset$ で $\prec,X$ を含まない文に限れば、$T$ は等号の扱いを除いて Peano算術 の記事の $\mathsf{PA}$ と同じ文を証明する（$\mathsf{PA}$ のモデルは $\prec$ と $X$ を空集合と解釈すれば $\mathsf{PA}(X)$ のモデルになること（$\prec,X$ の原子論理式を $\lnot(0=0)$ に置き換えると算術の言語の論理式になる）と、$\mathbf{LK}$ の完全性と等号の公理による帰着、Bus98 §2.1.3 p. 29、§2.2.3 p. 30、§2.3.7 pp. 33–36。この記事では証明しない）。
$T\vdash\varphi$ かつ $T\vdash\lnot\varphi$ なら $\lnot\mathrm L$ とカットで $\Gamma_0\Rightarrow$ が出る。
$T$ の各元 $\gamma$ について、ある $\delta<\omega^2$ で $\vdash^\delta_0\gamma^*$ である。
公理 1〜8、(E1)、$\mathcal S$ の元は lem-gcp-taut の 2 による。帰納法の公理は、$n$ 段の推論をすべての $n$ について並べて高さ $\omega$ の導出を作り、(E2) は lem-gcp-taut の 1 から有限の高さで得る。
帰納法の公理の導出を開く
帰納法の公理では、$\vec u$ に数項を代入した $F(x):=\varphi^*(x,\vec m)$、$r:=\operatorname{rk}F$、$E:=\exists x\,(F(x)\land\sim\!F(Sx))$ について、公理の否定標準形は $\forall\vec u\,((\sim\!F(0)\lor E)\lor\forall x\,F(x))$ である。$n$ についての帰納法で
$$\vdash^{2r+2n}_0\sim\!F(0),\,E,\,F(\underline n)$$
を示す。$n=0$ は lem-gcp-taut の 1。$n$ で成り立てば、$\vdash^{2r}_0\sim\!F(\underline{n+1}),F(\underline{n+1})$ と合わせて ($\land$) で $F(\underline n)\land\sim\!F(\underline{n+1})$ を作り、$S\underline n=\underline{n+1}$ なので ($\exists$) で $E$ の中へ入れると、$n+1$ で成り立つ。($\omega$) で高さ $\omega$、($\lor$) 4 回と $\vec u$ についての ($\omega$) で高さ $\omega+4+\lvert\vec u\rvert$ を得る。
(E2) の導出を開く
代入例 $\lnot(\underline n=\underline p)\lor(\sim\!F(\underline n)\lor F(\underline p))$ は、$n\ne p$ なら (Ax1) と ($\lor$) で高さ $1$、$n=p$ なら lem-gcp-taut の 1 と ($\lor$) 3 回で高さ $2r+3$ で導出できる。高さが一様に有限なので、($\omega$) を $2+\lvert\vec u\rvert$ 回使って有限の高さで (E2) を得る。$\square$
$\mathbf{LK}$ の導出の終列を $\Gamma\Rightarrow\Delta$、高さ（根から葉への道の上の規則の個数の最大値）を $h$ とし、すべてのカット論理式 $A$ で $\operatorname{rk}A^*< k$ とする。固有変数用の定数記号に数項を割り当てて置き換える操作を $(\cdot)^\rho$ とすると、すべての $\rho$ について $\vdash^{\omega+2h}_k\{\sim\!(A^*)^\rho\mid A\in\Gamma\}\cup\{(B^*)^\rho\mid B\in\Delta\}$ である。
導出の組み立てについての帰納法で、各規則を高々 2 回の規則で置き換える。始シークエントは lem-gcp-taut の 1 で高さ $2\operatorname{rk}A^*<\omega$。要所は量化の規則で、固有変数には数項をすべて代入して ($\omega$) を使う。
規則ごとの置き換えを開く
$\forall\mathrm R$（固有変数 $a$）では、$a$ だけを $\underline n$ に変えた割り当てで前提に帰納法の仮定を使う。$a$ は結論に現れないので、すべての $n$ について揃った前提に ($\omega$) を使える。$\forall\mathrm L$（閉項 $t$）では、$t^\rho$ の値を $m$ として lem-gcp-basic の 2 で $\underline m$ に取り替え、$\sim\forall x\,A^*=\exists x\,\sim\!A^*$ に ($\exists$) を使う。
$\exists\mathrm L$・$\exists\mathrm R$ は上の 2 つと双対である。弱化・縮約・交換は lem-gcp-basic の 1。カットは両前提を和集合まで弱化して (Cut)。$\lnot\mathrm L$・$\lnot\mathrm R$ は $\sim\sim\!A^*=A^*$ なので前提と結論の翻訳が同じ集合である。$\land,\lor$ の規則は ($\land$) か ($\lor$) を 1 回。${\to}\mathrm L$ は $\sim(A\to B)^*=A^*\land\sim\!B^*$ に ($\land$)、${\to}\mathrm R$ は $\sim\!A^*\lor B^*$ に ($\lor$) を 2 回使う。$\square$
$L$ の文 $\sigma$ について $T\vdash\sigma$ なら、ある $\alpha<\varepsilon_0$ について $\vdash^\alpha_0\sigma^*$ である。
$\mathbf{LK}\vdash\gamma_1,\dots,\gamma_j\Rightarrow\sigma$（$\gamma_i\in T$）の導出の高さを $h$ とし、$k$ をカット論理式と $\gamma_i^*$ のどの階数よりも大きくとる。lem-gcp-embed により $\vdash^{\omega+2h}_k\sim\!\gamma_1^*,\dots,\sim\!\gamma_j^*,\sigma^*$、lem-gcp-axioms により $\vdash^{\delta_i}_0\gamma_i^*$（$\delta_i<\omega^2$）である。$\delta:=\max(\omega+2h,\delta_1,\dots,\delta_j)$ とし、弱化してから $\gamma_1^*,\gamma_2^*,\dots$ の順にカットすると、$i$ 回目の後に $\vdash^{\delta+i}_k\sim\!\gamma_{i+1}^*,\dots,\sim\!\gamma_j^*,\sigma^*$ を得る。よって $\vdash^{\delta+j}_k\sigma^*$、thm-gcp-cut-elim の 2 により $\vdash^{\omega_k(\delta+j)}_0\sigma^*$ である。$\delta+j<\omega^2<\varepsilon_0$ なので lem-gcp-epsilon の 2 により $\omega_k(\delta+j)<\varepsilon_0$ である。$\square$
$T$ は矛盾しない。とくに $\mathsf{PA}(X)$ は矛盾しない。
$\mathbf{LK}\vdash\gamma_1,\dots,\gamma_j\Rightarrow$ なら、prf-gcp-main と同じ手順で、ある $\alpha$ について $\vdash^\alpha_0\emptyset$ を得る。しかしカット以外のどの条件も $\Gamma$ が元をもつことを求め、$k=0$ ではカットは使えない。$\square$
この系は $\mathsf{PA}$ の無矛盾性を含む。ただし議論は集合論の中で無限の導出と順序数を自由に使っている。
上限が改良できないこと
$\prec$ の解釈が 整礎関係 であるとする。$n$ の 階数 を $\lvert n\rvert:=\sup\{\lvert m\rvert+1\mid m\prec n\}$ で定め、$\|\prec\|:=\sup\{\lvert n\rvert+1\mid n\in\mathbb N\}$ とおく。整列順序なら $\|\prec\|$ はその順序型である。順序数 $\beta$ について $X_\beta:=\{n\mid\lvert n\rvert<\beta\}$ とし、$X$ を $X_\beta$ と解釈して文の集合 $\Gamma$ のどれかが真になることを「$\Gamma$ は $X_\beta$ のもとで真」という。$X$ について正な文は、$X_\beta$ のもとで真なら $\beta\le\beta'$ の $X_{\beta'}$ のもとでも真である。
$\prec$ に沿った超限帰納法を $\mathbf{LK}$ の文で $\mathrm{TI}(\prec,X):=\forall x\,\bigl(\forall y\,(y\prec x\to X(y))\to X(x)\bigr)\to\forall x\,X(x)$ と書く。否定標準形では、$P:=\exists x\,\bigl(\forall y\,(\lnot(y\prec x)\lor X(y))\land\lnot X(x)\bigr)$ について $\mathrm{TI}(\prec,X)^*=P\lor\forall x\,X(x)$ である。
$\Gamma'$ を $X$ について正な文の有限集合、$s_1,\dots,s_j$ を閉項（$j\ge0$）、$\gamma$ を順序数とし、すべての $i$ で $\lvert s_i^{\mathfrak N}\rvert<\gamma$ とする。$\vdash^\alpha_0P,\Gamma',\lnot X(s_1),\dots,\lnot X(s_j)$ なら、$\Gamma'$ は $X_{\gamma+\omega^\alpha}$ のもとで真である。
$\beta:=\gamma+\omega^\alpha$ とおき、最後の条件で分ける（カットはない）。要の場合は、主論理式が $P$ で、($\exists$) で数 $n$ を代入したときである。前提 $\vdash^{\alpha_0}_0P,\Gamma',\lnot X(\vec s),D$、$D:=\forall y\,(\lnot(y\prec\underline n)\lor X(y))\land\lnot X(\underline n)$ に逆転を $\land,\forall,\lor$ の順に使うと
(a) すべての $m$ で $\vdash^{\alpha_0}_0P,\Gamma',\lnot X(\vec s),\lnot(\underline m\prec\underline n),X(\underline m)$、(b) $\vdash^{\alpha_0}_0P,\Gamma',\lnot X(\vec s),\lnot X(\underline n)$
を得る。$\Gamma'$ が $X_\beta$ のもとで偽とすると、$X_{\gamma+\omega^{\alpha_0}}$ のもとでも偽である。$m\prec n$ なら偽のリテラル $\lnot(\underline m\prec\underline n)$ を (a) から除き（lem-gcp-basic の 3）、帰納法の仮定を使うと $X(\underline m)$ が $X_{\gamma+\omega^{\alpha_0}}$ のもとで真、すなわち $\lvert m\rvert<\gamma+\omega^{\alpha_0}$ である。よって $\lvert n\rvert\le\gamma+\omega^{\alpha_0}<\gamma':=\gamma+\omega^{\alpha_0}+1$。(b) に $\gamma'$ で帰納法の仮定を使うと、$\Gamma'$ は $X_{\gamma'+\omega^{\alpha_0}}$ のもとで真である。$1+\omega^{\alpha_0}\le\omega^{\alpha_0}\cdot2$ と lem-gcp-epsilon の 3 から $\gamma'+\omega^{\alpha_0}\le\gamma+\omega^{\alpha_0}\cdot3<\beta$ なので、$\Gamma'$ は $X_\beta$ のもとで真となり、矛盾する。
残りの場合を開く
- (Ax1)：真の $X$ を含まないリテラルは $\Gamma'$ にあり、$X$ の解釈によらず真である。
- (Ax2)：$\Gamma'$ は $\lnot X$ のリテラルを含まないので、組は $X(s)\in\Gamma'$ と $\lnot X(s_i)$ である。$\lvert s^{\mathfrak N}\rvert=\lvert s_i^{\mathfrak N}\rvert<\gamma\le\beta$ なので $X(s)$ は真である。
- 主論理式が $\Gamma'$ にある：前提で加わる論理式も $X$ について正である。各前提（高さ $\alpha_i<\alpha$）に帰納法の仮定を使うと、$\Gamma'$ と加わった論理式のどれかが $X_\beta$ のもとで真である。$\Gamma'$ が偽なら加わった論理式がすべての前提で真になり、規則の形から主論理式が真になる。
リテラルは主論理式にならないので、場合はこれで尽きる。$\square$
$\prec$ の解釈が整礎で $T\vdash\mathrm{TI}(\prec,X)$ なら、$\|\prec\|<\varepsilon_0$ である。とくに $\prec$ の解釈が順序型 $\varepsilon_0$ の整列順序なら、$X$ を含まない真な文をどれだけ公理に加えても $\mathrm{TI}(\prec,X)$ は証明できない。
thm-gcp-main により、ある $\alpha<\varepsilon_0$ で $\vdash^\alpha_0P\lor\forall x\,X(x)$ である。逆転を $\lor,\forall$ の順に使うと、すべての $n$ で $\vdash^\alpha_0P,X(\underline n)$。thm-gcp-bounded（$j=0$、$\gamma=0$、$\Gamma'=\{X(\underline n)\}$）により $\lvert n\rvert<\omega^\alpha$ である。よって $\|\prec\|\le\omega^\alpha<\varepsilon_0$ である。$\square$
逆に $\mathsf{PA}$ は、算術の論理式で書ける述語について $\varepsilon_0$ 未満の各順序数までの超限帰納法を証明する（Rat06 p. 47。この記事では証明しない）。この意味で $\varepsilon_0$ は上限である。
例
$\varphi(x):=X(x)$ の帰納法の公理の導出は高さ $\omega+4$ である。
高さの勘定を開く
$r=0$ で、prf-gcp-axioms の構成により $\vdash^{2n}_0\lnot X(0),E,X(\underline n)$、$\vdash^\omega_0\lnot X(0),E,\forall x\,X(x)$ となり、($\lor$) を 4 回使って高さ $\omega+4$ になる。高さ $\omega$ は $n$ 段の推論をすべての $n$ について並べることから生じる。
$\prec$ を通常の $<$ とすると $\lvert n\rvert=n$、$\|\prec\|=\omega$ である。
偶数を奇数より前に置く例を開く
偶数をすべて奇数より前に置き、偶数どうし・奇数どうしは通常の順序とすると、$\lvert 2i\rvert=i$、$\lvert 2i+1\rvert=\omega+i$ で $\|\prec\|=\omega\cdot2$ である。
反例：条件を外すと成り立たない
| 外す条件 | 反例 | 成り立たなくなること |
|---|---|---|
| 導出の木が整礎であること（高さ $\alpha$ をもつこと） | 下の 1 の、自分自身へ戻る木 | 空の列が導出できないこと |
| ($\omega$) がすべての $n$ の前提をもつこと（前提を $n=0$ だけにする） | $\{0=0\}$ から $\{\forall x\,(x=0)\}$ | 空の列が導出できないこと |
| $X$ が解釈をもたないこと（$X(x)$ を $X$ を含まない論理式に替える） | $X(x)$ を $x=x$ に替える | cor-gcp-ti の結論 $\|\prec\|<\varepsilon_0$ |
どの反例も、外した条件のもとで規則の形を満たす具体的な導出（または証明）を作れば確かめられる。
確かめを開く
1：$\emptyset$ を $0=0$ のカットで $\{0=0\}$（(Ax1)）と $\{\lnot(0=0)\}$ から得て、$\{\lnot(0=0)\}$ を同じカットで $\{\lnot(0=0),0=0\}$（(Ax1)）と $\{\lnot(0=0)\}$ 自身から得る。この操作を限りなく続けた木は各頂点で規則の形を満たすが、無限に下る道をもち高さを割り当てられない。
2：変えた規則で $\{0=0\}$ から $\{\forall x\,(x=0)\}$、(Ax1) と ($\exists$) で $\{\exists x\,\lnot(x=0)\}$（$\lnot(\underline1=0)$ は真）が出て、2 つは双対なのでカットで $\emptyset$ を得る。
3：$\forall x\,(\dots)\to\forall x\,(x=x)$ は (E1) と $\to\mathrm R$ で $T$ から証明でき、$\prec$ を順序型 $\varepsilon_0$ の整列順序にとれば $\|\prec\|=\varepsilon_0$ である。$X$ を含まない論理式では lem-gcp-taut の 2 のように真理が導出を与え、thm-gcp-bounded の議論が働かない。
補足：Gentzen の元の証明と有限の立場
Gentzen の元の方法と有限の立場での定式化を開く
Gentzen 自身は無限の導出を使わず、空の列を結論とする $\mathsf{PA}$ の有限の導出（矛盾の導出）があったとして、それに順序数を割り当てる方法を考案した（Rat06 p. 53）。
こうして主張は $\mathsf F+\text{EC-TI}(\varepsilon_0)\vdash\mathrm{Con}(\mathsf{PA})$ の形になる（$\mathsf F$ は有限的に正当化される推論を体現する理論、$\text{EC-TI}(\varepsilon_0)$ は初等的に計算可能な述語についての $\varepsilon_0$ までの超限帰納法。Rat06 式 (1)、p. 47）。無限の導出による議論からも、その細部を見直すと同じ形の証明が得られる（Rat06 p. 53。この記事では証明しない）。$\mathsf F$ は $\mathsf{PA}$ の部分理論にとれる（Rat06 p. 47）ので、第 2 不完全性定理と合わせると、$\mathsf{PA}$ は $\text{EC-TI}(\varepsilon_0)$ のすべての例を証明することはできない。
関連項目
- 前提: Peano算術, シークエント計算, 順序数, 超限帰納法
- 比較: 証明論, Gödelの不完全性定理, 無矛盾性
- 道具: 整礎関係
- 発展: Craigの補間定理, 逆数学
参考文献
Mathpediaは寄付と、参考文献の書籍リンク（Amazonアソシエイト）の紹介料で運営されています。 支援について ／ 寄付する
