Kreiselの反例

353

Gentzenは順序数 $ε_{0}$ を順序型として持つ順序数表記に対する超限帰納法からPeano算術の無矛盾性を示した。現代的に言えばGentzenの示したことは以下のように表すことができる。

Gentzenによる無矛盾性証明

ある $ε_{0}$ を順序型に持つ整列順序 $≺$ が存在し
$PRA + PR - TI (≺) ⊢ Con (PA)$ であり、かつ $≺$ の任意の始切片 $≺↾$ に対して、 $PRA + PR - TI (≺↾) ⊬ Con (PA)$ である。

このことから理論 $T$ の強さを表現するための不変量として以下のようなものを以下のように定義したくなる。

証明論的順序数??

理論 $T$ に対して順序数 $∥ T ∥_{Con}$ を、順序数 $α$ を標準モデルにて順序型に持つ整列順序 $≺$ が存在して $PRA + PR - TI (≺) ⊢ Con (T)$ となるような最小の $α$ とする。

この定義とGentzenの定理から $∥ PA ∥_{Con} = ε_{0}$ であることが期待されるだろう。しかしKreiselは任意の再帰的可算で無矛盾な理論 $T$ に対して $∥ T ∥_{Con} \leq ω$ であることを示した。以下ではそのKreiselの反例を算術的階層に一般化して示す。

算術的階層

$Δ_{0}^{0}$ を有界論理式全体の集合とする。
$Σ_{0}^{0} := Π_{0}^{0} := Δ_{0}^{0}$ とする。
$Σ_{n + 1}^{0}$ を、ある $φ (x) \in Π_{n}^{0}$ に対して $\exists x φ (x)$ と表せる論理式の集合とする。
$Π_{n + 1}^{0}$ を、ある $φ (x) \in Σ_{n}^{0}$ に対して $\forall x φ (x)$ と表せる論理式の集合とする。

超限帰納法図式

論理式 $x ≺ y$ 、論理式の集合 $Γ$ に対して $Γ - TI (≺)$ を以下のような図式とする。

$(\forall x \in field (≺)) [(\forall y ≺ x) φ (y) \to φ (x)] \to (\forall x \in field (≺)) φ (x)$ 、ここで $φ \in Γ$ とする。

採集公理図式

論理式の集合 $Γ$ に対して $B Γ$ を以下のような図式とする。

$(\forall u) [(\forall x < u) (\exists \vec{y}) φ (x, \vec{y}) \to (\exists v) (\forall x < u) (\exists \vec{y} < v) φ (x, \vec{y})]$ 、ここで $φ \in Γ$ とする。

$Γ$ を $n \geq 1$ に対して $Σ_{n}^{0}, Π_{n}^{0}$ のいずれかとする。また $Γ$ から有界量化に関して閉じた論理式のクラスを $BQ (Γ)$ とする。任意の $φ \in BQ (Γ)$ に対してある $ψ \in Γ$ が存在し $EA + B Γ ⊢ φ \leftrightarrow ψ$ である。

一般化されたKreiselの反例

任意の標準モデルで真な $Π_{n + 1}^{0}$ -論理式 $φ$ に対しある初等再帰的で標準モデルに於いて $ω$ を順序型として持つ整列順序 $≺_{φ}^{K}$ が存在し $EA + B Σ_{n}^{0} + Σ_{n}^{0} - TI (≺_{φ}^{K}) ⊢ φ$ であり、また $EA + Π_{n + 1}^{0} - TI (≺_{φ}^{K}) ⊢ φ$ である。

$φ :\Leftrightarrow \forall x φ_{0} (x)$ とし、 $≺_{φ}^{K}$ を以下のように定める。 $x ≺_{φ}^{K} y :\Leftrightarrow {\begin{cases} x < y & if (\forall i < x) φ_{0} (i) \\ y < x & otherwise \end{cases}$ まず $N ⊨ \forall x φ_{0} (x)$ と仮定しているから $N ⊨ (\forall i < x) φ_{0} (x)$ でありよって $N ⊨ x < y \leftrightarrow x ≺_{φ}^{K} y$ であり初等再帰的であることと順序型が $ω$ であることが分かる。

今、論理式 $φ^{'}$ を $φ^{'} (x) :\Leftrightarrow (\forall i \leq x) φ_{0} (i)$ とすれば $B Σ_{n}^{0}$ から $φ^{'}$ は適当な $Σ_{n}^{0}$ -論理式と同一視できる。そして $EA ⊢ (\forall y ≺_{φ}^{K} x) φ^{'} (y) \to φ^{'} (x)$ が成り立つ。これを背理法で示そう。 $\neg φ^{'} (x) \land (\forall y ≺_{φ}^{K} x) φ^{'} (y)$ であるとすると、 $\neg φ^{'} (x)$ から $(\exists i \leq x) \neg φ_{0} (x)$ であり、 $≺_{φ}^{K}$ の定義から $x + 1 ≺_{φ}^{K} x$ であり、よって $(\forall y ≺_{φ}^{K} x) φ^{'} (y)$ から $φ^{'} (x + 1)$ である。明らかに $φ^{'} (x + 1) \to φ^{'} (x)$ なので $φ^{'} (x)$ が成り立ち矛盾する。

上の議論から
$EA + B Σ_{n}^{0} + Σ_{n}^{0} - TI (≺_{φ}^{K}) ⊢ (\forall y ≺_{φ}^{K} x) φ^{'} (y) \to φ^{'} (x)$ であり、 $B Σ_{n}^{0}$ により $φ^{'}$ と同値な $Σ_{n}^{0}$ -論理式 $ψ$ を取れば
$EA + B Σ_{n}^{0} + Σ_{n}^{0} - TI (≺_{φ}^{K}) ⊢ (\forall y ≺_{φ}^{K} x) ψ (y) \to ψ (x)$ となる。よって $Σ_{n}^{0} - TI (≺_{φ}^{K})$ から $EA + B Σ_{n}^{0} + Σ_{n}^{0} - TI (≺_{φ}^{K}) ⊢ (\forall x) ψ (x)$ であり $ψ (x)$ と $φ^{'} (x)$ の同値性から $EA + B Σ_{n}^{0} + Σ_{n}^{0} - TI (≺_{φ}^{K}) ⊢ (\forall x) (\forall i \leq x) φ_{0} (i)$ となる。 $(\forall x) (\forall i \leq x) φ_{0} (i)$ は $\forall x φ_{0} (x)$ すなわち $φ$ と同値になる。 $EA + Π_{n + 1}^{0} - TI (≺_{φ}^{K}) ⊢ φ$ の方は $φ^{'}$ が $Π_{n + 1}^{0}$ -論理式になることから $Σ_{n}^{0}$ に落とさなくても良くなることによる。以上にて証明を終える。