Return to Answer

Here is the crucial sentence $\delta(d)$: $$\left( \exists x \in \omega^X : \phi(x) \right) \implies \exists z \in \omega^X : \phi(z) \ \wedge \ \forall w \in \omega^X : \phi(w)\! \implies \! \left( w \geq z \ \vee \ \forall_{e \geq d} : w_e=z_e \right) $$ In other words, $\delta(d)$ is essentially the induction claim $I(x,\omega^X, \phi)$, but we are allowed to have $w<z$ as long as $w$ and $z$ agree on the part of $X$ past $d$.

Here is the crucial sentence $\delta(d)$: $$\left( \exists x \in \omega^X : \phi(x) \right) \implies \\ {\big[} \exists z \in \omega^X : \phi(z) \ \wedge \ \forall w \in \omega^X : \phi(w)\! \implies \! \left( w \geq z \ \vee \ \forall_{e \geq d} : w_e=z_e \right) {\big]} $$ In other words, $\delta(d)$ is essentially the induction claim $I(x,\omega^X, \phi)$, but we are allowed to have $w<z$ as long as $w$ and $z$ agree on the part of $X$ past $d$.

The strategy of the proof is the only thing it could be. I will describe a recipe which, given a first order sentence $\phi(x)$, with $x$ ranging over $\omega^X$, produces a first order sentence $\phi'(x')$ with $x'$ ranging over $X$. I'll then show that $I(x', X, \phi')$ implies $I(x,\omega^X, \phi)$. The sentence $\phi'$ will have an extra $\exists \forall$ in front of whatever quantifiers $\phi$ has.

Write $\omega \uparrow n$ for a towers of $\omega$'s stacked $n$ high. Then this argument reduces proving $I(x,\omega \uparrow n, \phi)$ to proving $I(x', \omega \uparrow (n-1), \phi')$, and the reduces that to $I(x'', \omega \uparrow (n-2), \phi'')$ etcetera, until we finally reach $I(x^{n-1}, \omega, \phi^{n-1})$. In the process, we have added $n-1$ alternations of $\exists \forall$. Of course, $I(x^{n-1}, \omega, \phi^{n-1})$ is an axiom of PA, so we will then be done.

ADDED Eleizer Yudkowsky and Benedict Eastaugh point out below that I am doing something inefficient. My recursion turns $\Sigma_n$ statements about $\omega^X$ into $\Sigma_{n+2}$ statements about $X$, whereas I am only supposed to need to go from $n$ to $n+1$. See discussion below.

As you can see, $\delta$ sticks an extra $\exists \forall$ in front of $\phi$.

The strategy of the proof is the only thing it could be. I will describe a recipe which, given a first order sentence $\phi(x)$, with $x$ ranging over $\omega^X$, produces a first order sentence $\phi'(x')$ with $x'$ ranging over $X$. I'll then show that $I(x', X, \phi')$ implies $I(x,\omega^X, \phi)$. The sentence $\phi'$ will have three occurrences of $\phi$: One preceded by $\forall \neg$, one preceded by $\exists$ and one preceded by $\exists \forall \neg$. If $\phi$ is in $\Sigma_n$, then these are in $\Pi_n$, $\Sigma_n$ and $\Sigma_{n+1}$ respectively. I think this shows that this construction takes $\Sigma_n$ to $\Sigma_{n+1}$ (but I must admit that I am not fully confident in this argument.)

Write $\omega \uparrow n$ for a towers of $\omega$'s stacked $n$ high. Then this argument reduces proving $I(x,\omega \uparrow n, \phi)$ to proving $I(x', \omega \uparrow (n-1), \phi')$, and the reduces that to $I(x'', \omega \uparrow (n-2), \phi'')$ etcetera, until we finally reach $I(x^{n-1}, \omega, \phi^{n-1})$. In the process, we have added turned a $\Sigma_k$ statement into a $\Sigma_{k+n}$ statement. Of course, $I(x^{n-1}, \omega, \phi^{n-1})$ is an axiom of PA, so we will then be done.

Rewritten without $\implies$, this is of the form $$\forall_x \neg \phi(x) \vee \exists_z \left( \phi(z) \wedge \forall_w \neg \phi(w) \vee (\mbox{stuff without }\ \phi) \right).$$ So $\delta$ precedes $\phi$ with $\forall \neg$, with $\exists$ and with $\exists \forall \neg$ as promised.

ADDED Eleizer Yudkowsky and Benedict Eastaugh point out below that I am doing something inefficient. My recursion turns $\Sigma_n$ statements about $\omega^X$ into $\Sigma_{n+2}$ statements about $X$, whereas I am only supposed to need to go from $n$ to $n+1$. See discussion below.