S₂
定義
$ \mathrm S_2^i := \Sigma^b_i\text{-PIND}
$ \mathrm S_2 := \bigcup_i \mathrm S_2^i
定理
$ i \ge 1とする
$ \mathrm S_2^i \triangleq \Sigma^b_i\text{-PIND} = \Pi^b_i\text{-PIND} = \Sigma^b_i\text{-LIND} = \Pi^b_i\text{-LIND}
Proof.
$ \Sigma^b_i\text{-LIND} \vdash \Sigma^b_i\text{-PIND}
$ \Sigma^b_i 論理式$ \phi をとる。$ \Sigma^b_i\text{-LIND} \vDash \phi(0) \land (\forall x)[\phi(x/2) \to \phi(x)] \to (\forall x)\phi(x) を示せば良い あるモデル$ Mについて$ a \in Mが存在して
$ M \models \Sigma^b_i\text{-LIND}
$ M \models \phi(0) \land (\forall x)[\phi(x/2) \to \phi(x)] \land \lnot\phi(a)
と仮定する
以下のように$ \psi(x)を定義する。$ \psi(x)は$ \Sigma^b_i論理式である
$ \psi(x) := x \le |a| \to \phi(a|_x) := |a| \le x \lor (\exists y \le a)[a|_x = y \land \phi(y)]
$ (z|_x = y) := |y| = x \land (\exists w, l \le z)[|w| \le |l| \land |z| = |l| + |y|\land z = w + 2^{|l|} \cdot y]
左からの$ n桁部分列の長さは常に$ nだが右からはそうとは限らないため
また右からだと$ a|_x = a|_{x+1}/2が成り立たない
仮定より
$ M \models \psi(0)
$ M \models |0| = 0, $ M \models a = 0 + 2^{|0|} \cdot aなので$ M \models a|_0 = 0, $ M \models \psi(0)
$ M \models (\forall x)\lbrack\psi(x) \to \psi(x + 1)\rbrack
任意の$ x \in M, $ x+1 \le |a|, $ \psi(x)を固定する
$ M \models \phi(a|_x) より$ y \le a , $ a|_x = y , $ \phi(y) なる$ y \in Mが存在する
$ 2y+d \le a $ a|_{x+1} = 2y+dなる$ d < 2が存在する
$ |a| = |2y+d| + |l/2|, $ |w'| \le |l/2|,$ a = 2^{|l/2|} \cdot (2y+d) + w'を満たす$ d < 2, w' \le aが存在する
$ a|_x = yより$ |a| = |y| + |l|, $ |w| \le|l|,$ a = 2^{|l|} \cdot y + wを満たす$ l, w \le aが存在する
$ |y| + 1 = x + 1 \le |a|より$ l \ne 0, よって$ |l/2| + 1 = |l|, $ 2^{|l|} = 2 \cdot 2^{|l/2|}
剰余定理より$ w = 2^{|l/2|} \cdot d + w'を満たす$ w' < 2^{|l/2|}, $ d < 2が存在する $ w < 2^{|w|} = 2^{|l/2|} + 2^{|l/2|}より$ d < 2
よって$ a = 2^{|l|} \cdot y + (2^{|l/2|} \cdot d + w') = 2^{|l/2|}\cdot (2y + d) + w
また$ |a| = |y| + |l| = |y| + 1 + |l/2| = |2y+d| + |l/2|
また$ |w'| < |2^{|l/2|}| = |l/2| + 1より$ |w'| \le |l/2|
$ |2y + d| = |y| + 1 = x + 1より$ a|_x = 2y + d
$ a = 2^{|l/2|} \cdot (2y+d) + w'より$ 2y+d \le a
$ y = (2y+d)/2 なので$ M \models \phi(y) , 仮定$ M \models (\forall x)[\phi(x/2) \to \phi(x)]] より$ M \models \phi(a|_{x+1})
よって$ M \models \psi(x+1)
$ M \models \Sigma^b_i\text{-LIND} より$ M \models (\forall x)\psi(|x|)
よって$ M \models \psi(|a|), $ M \models \phi(a)
矛盾
$ \Sigma^b_i\text{-PIND} \vdash \Sigma^b_i\text{-LIND}
$ \Sigma^b_i 論理式$ \phi をとる。$ S_2^i \vDash \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \to (\forall x)\phi(|x|) を示せば良い。 あるモデル$ Mについて$ a \in Mが存在して
$ M \models \mathrm S_2^i
$ M \models \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \land \lnot\phi(|a|)
と仮定する
$ \psi(x) := \phi(|x|)と仮定する
このとき
$ \psi(0)
$ \psi(0) = \phi(0)
$ (\forall x)\lbrack \psi(x/2) \to \psi(x)\rbrack
$ x \in M, $ \psi(x/2) = \phi(|x/2|)を仮定する
$ M \models \Sigma^b_i\text{-PIND}より$ M \models (\forall x)\psi(x)
よって$ M \models \phi(|a|)
矛盾
$ \Sigma^b_i\text{-LIND} \vdash \Pi^b_i\text{-LIND}
$ \Pi^b_i 論理式$ \phi をとる。$ \Sigma^b_i\text{-LIND} \vDash \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \to (\forall x)\phi(|x|) を示せば良い。 あるモデル$ Mについて$ a \in Mが存在して
$ M \models \Sigma^b_i\text{-LIND}
$ M \models \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \land \lnot\phi(|a|)
と仮定する
$ \psi(x) := x \le a \to \lnot\phi(a-x) = x \le a \to (\exists y \le a)[a = x + y \land \lnot\phi(y)] と定義する
$ \psi(x)は$ \Sigma^b_i論理式 このとき
$ \psi(0)
$ a \le a, $ a = 0 + a, $ \lnot \phi(a)より$ \psi(0)
$ (\forall x)\lbrack \psi(x) \to \psi(x+1)\rbrack
$ x \in M,$ x + 1 \le a, $ \psi(x)を仮定する
$ x + 1 \le aより$ a = x + y + 1なる$ yが存在して$ \psi(x) \iff \lnot \phi(y + 1)
$ M \models \Sigma^b_i\text{-LIND}より$ M \models(\forall x)\psi(|x|)
よって$ M \models \psi(|a|) \iff M \models \lnot\phi(0)
$ \Pi^b_i\text{-LIND} \vdash \Sigma^b_i\text{-LIND}
上の証明で$ \psi(x) := x \le a \to \lnot\phi(a-x) = x \le a \to (\forall y \le a)[a = x + y \to \lnot\phi(y)] と置き換えて証明する
$ \Sigma^b_i\text{-PIND} \vdash \Pi^b_i\text{-PIND}
$ \Pi^b_i 論理式$ \phi をとる。$ \Sigma^b_i\text{-PIND} \vDash \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \to (\forall x)\phi(x) を示せば良い。 あるモデル$ Mについて$ a \in Mが存在して
$ M \models \Sigma^b_i\text{-PIND}
$ M \models \phi(0) \land (\forall x)[\phi(x) \to \phi(x + 1)] \land \lnot\phi(|a|)
と仮定する
$ \psi(x) := \lnot\phi(a/2^{|x|}) = (\exists y,z \le a)[z < 2^{|x|} \land a = 2^{|x|} \cdot y + z \land \lnot\phi(y)] と定義する
$ \psi(x)は$ \Sigma^b_i論理式 このとき
$ \psi(0)
$ a \le a, $ a = 2^{|0|} \cdot a$ \lnot\phi(a)より$ \psi(0)
$ (\forall x)\lbrack \psi(x/2) \to \psi(x)\rbrack
$ x \in M, $ \psi(x/2)を仮定する
$ \psi(x/2)より$ y,z \le a, $ z < 2^{|x/2|}が存在して$ a = 2^{|x/2|} \cdot y + z, $ \lnot\phi(y)
$ d < 2が存在して$ y = 2(y/2) + d
$ a = 2^{|x/2|}(2(y/2) + d) + z = 2^{|x|}(y/2) + (2^{|x/2|}\cdot d + w)より$ \psi(x)
$ M \models \Sigma^b_i\text{-PIND}より$ (\forall x)\psi(x)
よって$ M \models \psi(a)
$ y,z \le aが存在して$ a = 2^{|a|} \cdot y + z, $ \phi(y)よって$ y = 0, $ M \lnot\phi(0)
矛盾
$ \Pi^b_i\text{-PIND} \vdash \Sigma^b_i\text{-PIND}
上の証明で$ \psi(x) := \lnot\phi(a/2^{|x|}) = (\forall y,z \le a)[z < 2^{|x|} \land a = 2^{|x|} \cdot y + z \to \lnot\phi(y)] と置き換えて証明する
関連