Kreiselの反例
Gentzenは順序数$\varepsilon_0$を順序型として持つ順序数表記に対する超限帰納法からPeano算術の無矛盾性を示した。現代的に言えばGentzenの示したことは以下のように表すことができる。
ある$\varepsilon_0$を順序型に持つ整列順序$\prec$が存在し
$$\mathsf{PRA}+\mathsf{PR}\text{-}\mathsf{TI}(\prec)\vdash\mathsf{Con}(\mathsf{PA})$$であり、かつ$\prec$の任意の始切片$\prec\restriction$に対して、$$\mathsf{PRA}+\mathsf{PR}\text{-}\mathsf{TI}(\prec\restriction)\nvdash\mathsf{Con}(\mathsf{PA})$$である。
このことから理論$T$の強さを表現するための不変量として以下のようなものを以下のように定義したくなる。
理論$T$に対して順序数$\|T\|_{\mathsf{Con}}$を、順序数$\alpha$を標準モデルにて順序型に持つ整列順序$\prec$が存在して$$\mathsf{PRA}+\mathsf{PR}\text{-}\mathsf{TI}(\prec)\vdash\mathsf{Con}(\mathsf{T})$$となるような最小の$\alpha$とする。
この定義とGentzenの定理から$\|\mathsf{PA}\|_{\mathsf{Con}}=\varepsilon_0$であることが期待されるだろう。しかしKreiselは任意の再帰的可算で無矛盾な理論$T$に対して$\|T\|_{\mathsf{Con}}\leq\omega$であることを示した。以下ではそのKreiselの反例を算術的階層に一般化して示す。
- $\Delta^0_0$ を有界論理式全体の集合とする。
- $\Sigma^0_0:=\Pi^0_0:=\Delta^0_0$ とする。
- $\Sigma^0_{n+1}$ を、ある $\varphi(x)\in\Pi^0_n$ に対して $\exists x\varphi(x)$ と表せる論理式の集合とする。
- $\Pi^0_{n+1}$ を、ある $\varphi(x)\in\Sigma^0_n$ に対して $\forall x\varphi(x)$ と表せる論理式の集合とする。
論理式$x\prec y$、論理式の集合$\Gamma$に対して$\Gamma\text{-}\mathsf{TI}(\prec)$を以下のような図式とする。
- $(\forall x\in\mathrm{field}(\prec))[(\forall y\prec x)\varphi(y)\to\varphi(x)]\to(\forall x\in\mathrm{field}(\prec))\varphi(x)$、ここで$\varphi\in\Gamma$とする。
論理式の集合$\Gamma$に対して$\mathsf{B}\Gamma$を以下のような図式とする。
- $(\forall u)[(\forall x\lt u)(\exists \vec{y})\varphi(x,\vec{y})\to(\exists v)(\forall x\lt u)(\exists \vec{y}\lt v)\varphi(x,\vec{y})]$、ここで$\varphi\in\Gamma$とする。
$\Gamma$を$n\geq 1$に対して$\Sigma^0_n,\Pi^0_n$のいずれかとする。また$\Gamma$から有界量化に関して閉じた論理式のクラスを$\mathcal{BQ}(\Gamma)$とする。任意の$\varphi\in\mathcal{BQ}(\Gamma)$に対してある$\psi\in\Gamma$が存在し$\mathsf{EA}+\mathsf{B}\Gamma\vdash\varphi\leftrightarrow\psi$である。
任意の標準モデルで真な$\Pi^0_{n+1}$-論理式$\varphi$に対しある初等再帰的で標準モデルに於いて$\omega$を順序型として持つ整列順序$\prec^\mathrm{K}_{\varphi}$が存在し$$\mathsf{EA}+\mathsf{B}\Sigma^0_n+\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash\varphi$$であり、また$$\mathsf{EA}+\Pi^0_{n+1}\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash\varphi$$である。
$\varphi:\Leftrightarrow\forall x\varphi_0(x)$とし、$\prec^\mathrm{K}_{\varphi}$を以下のように定める。$$x\prec^\mathrm{K}_{\varphi} y:\Leftrightarrow\begin{cases}x\lt y & \text{if }(\forall i\lt x)\varphi_0(i)\\ y\lt x &\text{otherwise}\end{cases}$$まず$\mathbb{N}\models\forall x\varphi_0(x)$と仮定しているから$\mathbb{N}\models (\forall i\lt x)\varphi_0(x)$でありよって$\mathbb{N}\models x\lt y\leftrightarrow x\prec^\mathrm{K}_{\varphi} y$であり初等再帰的であることと順序型が$\omega$であることが分かる。
今、論理式$\varphi'$を$\varphi'(x):\Leftrightarrow(\forall i\leq x)\varphi_0(i)$とすれば$\mathsf{B}\Sigma^0_n$から$\varphi'$は適当な$\Sigma^0_n$-論理式と同一視できる。そして$$\mathsf{EA}\vdash(\forall y\prec^\mathrm{K}_{\varphi} x)\varphi'(y)\to\varphi'(x)$$が成り立つ。これを背理法で示そう。$\lnot\varphi'(x)\land(\forall y\prec^\mathrm{K}_{\varphi} x)\varphi'(y)$であるとすると、$\lnot\varphi'(x)$から$(\exists i\leq x)\lnot\varphi_0(x) $であり、$\prec^\mathrm{K}_{\varphi}$の定義から$x+1\prec^\mathrm{K}_{\varphi} x$であり、よって$(\forall y\prec^\mathrm{K}_{\varphi} x)\varphi'(y)$から$\varphi'(x+1)$である。明らかに$\varphi'(x+1)\to\varphi'(x)$なので$\varphi'(x)$が成り立ち矛盾する。
上の議論から
$$\mathsf{EA}+\mathsf{B}\Sigma^0_n+\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash(\forall y\prec^\mathrm{K}_{\varphi} x)\varphi'(y)\to\varphi'(x)$$であり、$\mathsf{B}\Sigma^0_n$により$\varphi'$と同値な$\Sigma^0_n$-論理式$\psi$を取れば
$$\mathsf{EA}+\mathsf{B}\Sigma^0_n+\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash(\forall y\prec^\mathrm{K}_{\varphi} x)\psi(y)\to\psi(x)$$となる。よって$\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})$から$$\mathsf{EA}+\mathsf{B}\Sigma^0_n+\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash(\forall x)\psi(x)$$であり$\psi(x)$と$\varphi'(x)$の同値性から$$\mathsf{EA}+\mathsf{B}\Sigma^0_n+\Sigma^0_n\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash(\forall x)(\forall i\leq x)\varphi_0(i)$$となる。$(\forall x)(\forall i\leq x)\varphi_0(i)$は$\forall x\varphi_0(x)$すなわち$\varphi$と同値になる。$$\mathsf{EA}+\Pi^0_{n+1}\text{-}\mathsf{TI}(\prec^\mathrm{K}_{\varphi})\vdash\varphi$$の方は$\varphi'$が$\Pi^0_{n+1}$-論理式になることから$\Sigma^0_n$に落とさなくても良くなることによる。以上にて証明を終える。
再帰的可算かつ無矛盾な理論$T$に対し$\omega$を順序型として持つ整列順序$\prec^\mathrm{K}_T$が存在し$$\mathsf{EA}+\Sigma^0_0\text{-}\mathsf{TI}(\prec^\mathrm{K}_T)\vdash\mathsf{Con}(T)$$が成り立つ。
まず$\mathsf{EA}\vdash\mathsf{B}\Sigma^0_0$である。後は$\prec^\mathrm{K}_T:\Leftrightarrow \prec^\mathrm{K}_{\mathsf{Con}(T)}$とし一般化されたKreiselの反例による。
参考文献
- G. Kreisel, Wie die Beweistheoire zu ihren Ordinalzahlen kam und kommt, Jber. Deutsch. Math.-Verein 78, 177–223, 1977.