Σᵇ₀(Σᵇᵢ)-内包図式 (S₂)
$ \Sigma^b_0(\Sigma^b_i)-comprehention schema in $ \mathsf S_2^i
$ \mathrm{bit}(w, i + 1)の理由が分からなかったので$ \mathrm{bit}(w, i)と書いているが，問題ないと思う
定理
$ i \ge 1, $ \Sigma^b_0(\Sigma^b_i)論理式$ \alpha(\vec{u},i)について
$ \mathsf S_2^i \vdash (\exists w)(\forall i < \|y\|)[\alpha(\vec{u},i) \leftrightarrow \mathrm{bit}(w, i) = 1]
proof.
まず次を示す
すべての$ \Sigma^b_i論理式$ \alpha(\vec{u}, \vec{i})について
$ \mathsf{S}_2^i \vdash (\exists w)(\forall \vec{i} < \|\vec{y}\|)[\alpha(\vec{u}, \vec{i}) \leftrightarrow \mathrm{bit}(w, \braket{\vec{i}})]
$ \braket{\vec{i}}は
$ \braket{\vec{i}} \coloneqq i_0 + \|y_0\| i_1 + \|y_0\| \|y_1\| i_2 + \cdots + \|y_0\|\|y_1\| \cdots \|y_{k-2}\| i_{k-1}の略記
$ \vec{i} \mapsto \braket{\vec{i}}は
$ \Sigma^b_1定義可能
$ \mathsf S^1_2 \vdash 単射 であればなんでもよい
$ \beta(z) \coloneqq (\exists w \le \tau(\|\vec{y}\|) \left[\mathrm{nuon}(w) \ge z \land (\forall \vec{i} < \|\vec y\|)[\mathrm{bit}(w, \braket{\vec{i}}) \to \alpha(\vec u, \vec i)] \right]
ここで$ \|w\| < \braket{\|\vec{y}\|} \implies w \le \tau(\|\vec{y}\|)となるように$ \tauを十分大きくとる
次が成り立つ
$ \beta(0)
$ w \coloneqq \empty = 0を与えればよい
$ \lnot \beta(\|2\tau(\|\vec y\|)\|)
$ \beta(\|2\tau(\|\vec y\|)\|)であるような$ wが存在するなら
$ \|2\tau(\|\vec{y}\|)\| \le \mathrm{nuon}(w) \le \|w\| \le \|\tau(\|\vec{y}\|)\|より矛盾
$ \mathsf{LIND}\Sigma^b_iより$ \beta(z), $ \lnot \beta(z + 1)であるような$ zが存在する
$ \beta(z) のwitness$ w を固定する．
$ \vec{i} < \|\vec{y}\| を任意にとる．$ \alpha(\vec{u}, \vec{i}) \iff \mathrm{bit}(w, \braket{\vec{i}}) を示す．
$ \Leftarrowは$ \beta(z)よりあきらか
$ \Rightarrowを示す．
$ \alpha(\vec{u}, \vec{i})かつ$ \lnot\mathrm{bit}(w, \braket{\vec{i}})と仮定する．
このとき，$ wのインデックス$ \braket{\vec{i}}の値のみを$ 1に置き換えた列$ w'が存在する
$ z \le \mathrm{nuon}(w)より$ z + 1 \le \mathrm{nuon}(w')．なので，
よって$ w'は$ \beta(z + 1)のwitnessである．矛盾．
次は明らか
$ \mathsf{S_2^1} \vdash (\forall w_1, w_2)(\exists w \le 2\max(w_1, w_2))(\forall i \le |w|)[\mathrm{bit}(w, i) = 1 \leftrightarrow \mathrm{bit}(w_1, i) = 1 \lor \mathrm{bit}(w_2, i) = 1]
$ \mathsf{S_2^1} \vdash (\forall w_1, w_2)(\exists w \le 2\max(w_1, w_2))(\forall i \le |w|)[\mathrm{bit}(w, i) = 1 \leftrightarrow \mathrm{bit}(w_1, i) = 1 \land \mathrm{bit}(w_2, i) = 1]
これらから従う
系
$ \mathsf S^2_i \vdash \mathsf{LIND}(\Sigma^b_0(\Sigma^b_i))
Proof.
$ \varphi(x) \in \Sigma^b_0(\Sigma^b_i)
$ \mathrm{bit}(w, i) = 1は$ \Sigma^b_1なので $ \mathsf S_2^i \vdash \mathsf{LIND}(\Sigma^b_1)より