T₂ - 国立公園

T₂

#理論

#限定算術

定義

T₂はBASICに鋭限定論理式の帰納法図式を加えたS₂の言語の理論である

$ {\rm T}_2^i := \Sigma^b_i\text{-IND}

$ \mathrm T_2 := \bigcup_i \mathrm T_2^i

定理

$ i \ge 1とする

$ \mathrm T_2^i \triangleq \Sigma^b_i\text{-IND} = \Pi^b_i\text{-IND}

Proof.

$ \Sigma^b_i\text{-IND} \vdash \Pi^b_i\text{-IND}

$ \Pi^b_i 論理式$ \phi について$ \mathrm T_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 \Sigma^b_i\text{-IND}

$ 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 = 0 + a, $ \lnot\phi(a)より$ \psi(0)

❏

$ (\forall x)\lbrack\psi(x) \to \psi(x+1)\rbrack

$ x \in M, $ \psi(x), $ x + 1 \le aを固定する

$ \psi(x)より$ y \le aが存在して$ a = x + y + 1, $ \lnot\phi(y+1)

T₂#6472f7714507aa00005358c0より$ \lnot \phi(y)よって$ a = (x + 1) + yより$ \psi(x+1)

❏

$ M \models \Sigma^b_i\text{-IND}より$ (\forall x)\psi(x)

よって$ \psi(a), $ \lnot\phi(0)

矛盾

❏

$ \Pi^b_i\text{-IND} \vdash \Sigma^b_i\text{-IND}

上の証明で$ \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)] と置き換えて証明する

❏

定理

$ i \ge 1とする

$ \mathrm S_2^i \subseteq \mathrm T_2^i \subseteq \mathrm S_2^{i+1}

Proof.

$ \mathrm T_2^i \vdash \mathrm S^i_2

$ \mathrm T_2^i \vdash \phi(0) \land (\forall x)[\phi(x) \to \phi(x+1)] \to (\forall x)\phi(x) より

$ \mathrm T_2^i \vdash \phi(0) \land (\forall x)[\phi(x) \to \phi(x+1)] \to (\forall x)\phi(|x|)

$ \mathrm S_2^i = \Sigma^b_i\text{-LIND}(S₂#647139f54507aa0000ec1aab)より$ \mathrm T_2^i \vdash \mathrm S^i_2

$ \mathrm S_2^{i+1} \vdash \mathrm T_2^i

$ \mathrm S_2^{i+1} \nvdash \mathrm T_2^iと仮定する

以下を満たす$ M, $ \Sigma^b_i論理式$ \phi(x)が存在する

$ M \models \mathrm S_2^{i+1}

$ M \models \phi(0) \land (\forall x)[\phi(x) \to \phi(x+1)] \land \lnot\phi(a)

$ \Pi^b_{i+1}論理式$ \psi(x)を以下のように定義する

$ \psi(x) := (\forall y \le a)[\phi(y) \to \phi(x + y)]

このとき

$ (\forall x)\lbrack \psi(x/2) \to \psi(x) \rbrack

$ x \in M, $ \psi(x/2), $ y \le a, $ \phi(y)を固定する

$ \psi(x/2), $ \phi(y)より$ \phi(x/2+x/2+y)

よって$ \phi(x+y)

$ x = x/2 + x/2 + dなる$ d < 2が存在する

$ d = 0のとき$ \phi(x/2+x/2+y)よりあきらか

$ d = 1のときT₂#64753d424507aa00000d2628より$ \phi(x/2 + x/2 + y + 1)

あきらかに$ \psi(0)なので$ \mathrm{PIND}\psiより$ (\forall x)\psi(x)

S₂#646d79274507aa0000f721ecより$ M \models \Pi^b_{i+1}\text{-PIND}

$ \phi(0)より$ \phi(a)

矛盾

❏

系

$ \mathrm S_2 = \mathrm T_2