overspillとunderspill

適当な和訳があった気がするが思い出せない

定理

$ M \models \mathrm{I\Sigma_n}と仮定する

$ \Sigma_0(\Sigma_n)論理式$ \phi

任意の$ \vec v \in M, $ a \in Iについて$ M \models \phi(\vec v, a)ならばある$ b \in M\backslash Iが存在して$ M \models(\forall x \le b)\phi(\vec v, x)

任意の$ \vec v \in M, $ a \in M \backslash Iについて$ M \models \phi(\vec v, a)ならばある$ b \in Iが存在して$ M \models (\forall x > b)\phi(\vec v, x)

https://scrapbox.io/files/6491d7165553ae001c89b32f.png

Proof.

任意の$ b \in M\backslash Iについて$ M \models (\exists x \le b)\lnot\phi(\vec v, x)と仮定する

よって$ I = \{a \in M|(\forall x \le a)\phi(\vec v, x)\}

$ \Sigma_0(\Sigma_n)論理式$ \psi(\vec v, y) := (\forall x \le y)\phi(\vec v, x)の帰納法より$ M \models (\forall y) \psi(\vec v, y)

よって$ I = M. 矛盾

任意の$ b \in Iについて$ M \models (\exists x > b)\lnot\phi(\vec v, x)と仮定する

よって$ I = \{a \in M | (\exists x > a)\lnot\phi(\vec v, x)\}

$ \Sigma_0(\Sigma_n)論理式$ \psi(\vec v, y) := (\exists x > y)\phi(\vec v, x)の帰納法より$ M \models (\forall y) \psi(\vec v, y)

よって$ I = M. 矛盾