A theorem on the second-order arithmetic with the $\omega$ -rule
Moto-o Takahashi · Journal of the Mathematical Society of Japan · 1970
\ulcorner\varphi^{\urcorner}$ called the Godel number (abbreviated by G. $n.$ ) of $\varphi$ , satisfying the follow- ing conditions:1.1.1.If $\varphi$ and $\psi$ are distinct, then $\ulcorner\varphi^{\urcorner} eq\ulcorner\psi^{\urcorner}$ ; 1.1.2.The number-theoretic predicates, $F(a),$ $AX(a)$ , $C(a, b, c)$ , $UF_{0}(a)$ , $UF_{1}(a)$ and $FO(a, b)$ defined below are recursive;1.1.2.3.$C(a, b, c)\equiv\{a=\ulcorner\varphi^{\urcorner},$ $b=\ulcorner\psi^{\urcorner},$ $c=\ulcorner\chi^{\urcorner 1}$ and $\varphi$ is the consequence of $\psi$ and $\chi$ by modus ponens}, 1.1.2.4.$UF_{0}(a)\equiv\{a$ is the G. $n$ . of a formula of the form $(x)\varphi$ , where $x$ is a number variable}; 1.1.2.5.$UF_{1}(a)\equiv\{a$ is the G. $n$ . of a formula of the form $(\alpha^{k})\varphi$ where $\alpha^{k}$ is a function variable}; 1.1.2.6.$FO(a, b)\equiv\{b$ is the G. $n$ . of a function variable and it does not occur in the formula whose G. $n$ . is $a$ } ; 1.1.3.There exist recursive functions $g_{0}(a, b),$ $g_{1}(a, b)$ and $v(a, b)$ such that 1.1.3.1.whenever $a=\ulcorner(x)\varphi(x)^{\urcorner},$ $g_{0}(a, n)=\ulcorner\varphi(\overline{n})^{\urcorner}$ , where $\overline{n}$ is the numeral for a natural number $n$ ;1.1.3.2.whenever $a=\ulcorner(\alpha^{k})\varphi(\alpha^{k})^{\urcorner}$ and $b=\ulcorner\beta^{k\urcorner},$ $g_{1}(a, b)=\ulcorner\varphi(\beta^{k})^{ eg}$ ;1.1.3.3.whenever $a=\ulcorner\varphi^{\urcorner}$ and $b=\ulcorner\psi^{\urcorner},$ $v(a, b)=\ulcorner\varphi\vee\psi^{\urcorner}$ .Now we define predicates $Pr(a),$ $P^{*}(p)$ and $Pr^{*}(a)$ as follows:1.2.1.If $AX(a)$ , then $Pr(a)$ ; 1.2.2.If $Pr(b),$ $Pr(c)$ and $C(a, b, c)$ , then $Pr(a)$ ; 1.2.3.If $UF_{0}(a)$ and $Pr(g_{0}(a, n))$ for all $n$ , then $Pr(a)$ ; 1.2.4.If $UF_{1}(a),$ $FO(a, b)$ and $Pr(g_{1}(a, b))$ , then $Pr(a)$ ;1.2.5.$Pr(a)$ , only as required by 1.2.1-4.1.3.1.If $AX(a)$ , then $P^{*}(3^{a})$ ; 1.3.2.$P^{*}(p),$ $P^{*}(q)$ and $C(a, (p)_{1},$ $(q)_{1})$ , then $P^{*}(2\cdot 3^{a}5^{p}7^{q})$ ; 1.3.3.If $UF_{0}(a)$ and, for any $n,$ $P^{*}(\{e\}(n))$ and $(\{e\}(n))_{1}=g_{0}(a, n)$ , then $P^{*}(2^{2}\cdot 3^{a}\cdot 5^{e})$ ;1.3.4.If $UF_{1}(a),$ $FO(a, b),$ $P^{*}(p)$ and $(p)_{1}=g_{1}(a, b)$ , then $P^{*}(2^{3}3^{a}5^{b}7^{p})$ ; 1.3.5.$P^{*}(p)$ , only as required by 1.3.1-4.1.4.$Pr^{*}(a)\equiv\exists p[P^{*}(p)\wedge(p)_{1}=a]$ .If $P^{*}(p)$ and $(p)_{1}=\ulcorner\varphi^{\urcorner}$ , we say that $p$ is a recursive proof of $\varphi$ and $\varphi$ is recursively provable.It is clear that 1.5.$Pr(a)$ if and only if $a$ is the G. $n$ . of a formula provable in $A_{\omega}$ ;and that 1.6.If $Pr^{*}(a)$ , then $Pr(a)$ .The converse of 1.6 will give the affirmative answer to Shoenfield's problem,