狭義の有界量化子による帰納法と(広義の)有界量化子による帰納法は等価
言語$ L \supseteq L_\mathrm{OR}
$ (Q x \le y)の形の有界量化子のみを持つ言語$ Lの$ \Sigma_n論理式のクラスを$ \Sigma^{L,\mathrm{var}}_nと表記する $ (Q x \le t(\vec y))を有界量化子に含む言語$ Lの$ \Sigma_n論理式のクラスを$ \Sigma^{L,\mathrm{term}}_nと表記する 仮定
理論$ T_0
言語$ L の任意の$ k アリティ関数記号$ f について $ T_0 \vdash (\forall \vec x, \vec x')\left[\left(\bigwedge_i x_i \le x'_i\right) \to f(\vec x) \le f(\vec x')\right]
$ L = L_\mathrm{OR}, $ T \vdash \mathrm{I_{open}}ならばこれは成り立つ
補題
$ t(\vec x) \in \mathrm{Term}_L^k
$ T \vdash (\forall \vec x, \vec x')\left[\left(\bigwedge_i x_i \le x'_i\right) \to t(\vec x) \le t(\vec x')\right]
定理
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 = \mathrm{I\Sigma}^{L,\mathrm{term}}_n + T_0
Proof.
$ \mathrm{I\Sigma}^{L,\mathrm{term}}_n + T_0 \vdash \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0
はあきらか
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash \mathrm{I\Sigma}^{L,\mathrm{term}}_n + T_0
$ \phi(\vec x, z) \in \Sigma^\mathrm{term}_n を固定する.
以下を満たす$ \Sigma_0(\Sigma_n^{L, \mathrm{var}})論理式$ \phi_0(y, \vec x, z), 項$ s(\vec x, z)が存在する $ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall \vec x, z)(\forall y \ge s(\vec x, z))[\phi(\vec x, z) \leftrightarrow \phi_0(y, \vec x, z)]
Proof.
$ \phiの複雑性に関する帰納法
原子論理式のリテラル
$ s(\vec x, z) := \overline 0
$ \phi_0(y,\vec x, z) := \phi(\vec x, z)
$ \land, \lor
$ \phi(\vec x, z) = \phi_1(\vec x, z) \odot \phi_2(\vec x, z)のとき
$ \odot \in \{\land, \lor\}
仮定
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall \vec x, z)(\forall y \ge s_1(\vec x, z))[\phi_1(\vec x, z) \leftrightarrow \phi_{1,0}(y, \vec x, z)]
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall \vec x, z)(\forall y \ge s_2(\vec x, z))[\phi_2(\vec x, z) \leftrightarrow \phi_{2,0}(y, \vec x, z)]
$ s(\vec x, z) := s_1(\vec x, z) + s_2(\vec x, z)
$ \phi_0(y, \vec x, z) := \phi_{1,0}(y, \vec x, z) \odot \phi_{2,0}(y, \vec x, z)
$ (\forall x < t(\vec x, z)), (\exists x < t(\vec x, z))
$ \phi(\vec x, z) = (Q u \le t(\vec x, z))\phi'(u, \vec x, z)のとき
$ Q \in \{\forall, \exists\}
仮定
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall u, \vec x, z)(\forall y \ge s'(u, \vec x, z))[\phi'(u, \vec x, z) \leftrightarrow \phi'_0(y, u, \vec x, z)]
$ s(\vec x, z) := s'(t(\vec x, z), \vec x, z) + t(\vec x, z)
$ \phi_0(y, \vec x, z) := (Q u \le y)[u \le t(\vec x, z) \triangleright \phi_0'(y,u,\vec x, z)]
$ \triangleright = \begin{cases} \to & \text{if $Q = \forall$} \\ \land & \text{if $Q = \exists$} \end{cases}
このとき$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall \vec x, z)(\forall y \ge s(\vec x, z))[\phi(\vec x, z) \leftrightarrow \phi_0(y, \vec x, z)]
$ y \ge s(\vec x, z) ならば
$ \phi_0(y,\vec x, z) \leftrightarrow (Q u \le t(\vec x, z))\phi_0'(y, u, \vec x, z)
$ T_0 \vdash t(\vec x, z) \le s(\vec x, z) より
$ \leftrightarrow (Q u \le t(\vec x, z))\phi'(u, \vec x, z) \leftrightarrow \phi(\vec x, z)
$ T_0 \vdash (\forall u \le t(\vec x, z))[s'(u,\vec x, z) \le s(\vec x, z)]
より$ u \le t(\vec x, z))ならば$ s'(u, \vec x, z) \le s(\vec x, z) \le yだから仮定より成り立つ
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash \mathrm L\phi を示す
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash (\forall \vec x)[(\exists z)\phi(\vec x, z) \to (\exists z)[\phi(\vec x, z) \land (\forall z' \le z)\lnot\phi(\vec x, z')]]
$ \phi(\vec x, z)と仮定する
$ \phi(\vec x, z) \leftrightarrow \phi_0(s(\vec x, z), \vec x, z) より$ (\exists v)[\phi_0(s(\vec x, z), \vec x, v) \land (\forall v' \le v)\lnot\phi_0(s(\vec x, z), \vec x, v')]]
$ \mathrm{I\Sigma}^{L,\mathrm{var}}_n + T_0 \vdash \mathrm L\phi_0 に$ y := s(\vec x,z)を代入する
$ vを固定すると$ \phi(\vec x, v) \leftrightarrow \phi_0(s(\vec x, z), \vec x, v)より
$ \phi(\vec x, v), $ (\forall v' \le v)\lnot\phi(\vec x, v')
$ v \le zなので$ s(\vec x, v) \le s(\vec x, z)だから
参考