Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA? It is well-known that $\mathbf{PRA}$ plus $\epsilon_0$-induction on bounded formulas cannot prove all $\mathbf{PA}$ theorems (essentially because $I\Sigma_1$ plus $\epsilon_0$-induction on bounded formulas is finitely axiomatizable while the latter isn't). Are there any concrete examples known (preferable "natural")?
(This is an exact copy of my question on MSE, but I expect I won't get any answer there, so I hope I'm allowed to cross-post it here)
 A: One example is $I\Sigma_2$ (or rather, the conjunction of its finite axiomatization).
Notice that the theory $I\Sigma_1+\epsilon_0$-induction for bounded formulas is axiomatized by $\Pi_3$ sentences: in particular, the $\epsilon_0$-induction schema can be written in prenex form as
$$\forall u\,\forall x\,\exists y\,\forall z\,\bigl[\bigl(\neg\theta(u,y)\land(z\prec y\to\theta(u,z))\bigr)\lor\theta(u,x)\bigr],$$
where $\theta\in\Delta_0$ and $\prec$ is the order representing $\epsilon_0$. By a theorem of Leivant [1], $I\Sigma_2$ is not provable from any set of $\Pi_3$ (or even $\Sigma_4$) sentences consistent with $Q$. More generally, for $n\ge1$, $I\Sigma_n$ is not provable from any set of $\Sigma_{n+2}$ sentences consistent with $Q$.
The reason is that $I\Sigma_n$ proves the uniform $\Sigma_{n+1}$-reflection schema for $Q$:
$$\mathrm\forall x\,\bigl(\mathrm{Pr}_Q(\ulcorner\phi(\dot x)\urcorner)\to\phi(x)\bigr),\qquad\phi\in\Sigma_{n+1},$$
where $\mathrm{Pr}_Q$ denotes the formalized provability predicate for $Q$. This schema is equivalent to the single sentence
$$\def\rfn{\mathrm{RFN}}\rfn_Q(\Sigma_{n+1})=\forall x\,\bigl(\mathrm{Pr}_Q(x)\to\mathrm{Tr}_{n+1}(x)\bigr),$$
where $\mathrm{Tr}_{n+1}$ is the truth definition for $\Sigma_{n+1}$-formulas (defined so that it is vacuously true for non-$\Sigma_{n+1}$-formulas). Moreover, it is easy to see that
$$\rfn_Q(\Sigma_{n+1})\equiv\rfn_Q(\Pi_{n+2}).$$
Now, if we assume for contradiction that $\rfn_Q(\Pi_{n+2})$ is provable from a consistent extension of $Q$ by $\Sigma_{n+2}$ sentences, there is a single $\Sigma_{n+2}$ sentence $\phi$ consistent with $Q$ such that
$$Q+\phi\vdash\rfn_Q(\Pi_{n+2})\vdash\mathrm{Pr}_Q(\ulcorner\neg\phi\urcorner)\to\neg\phi,$$
that is,
$$Q+\phi\vdash\mathrm{Con}_{Q+\phi},$$
contradicting the second incompleteness theorem.
Reference:
[1] Daniel Leivant: The optimality of induction as an axiomatization of arithmetic, Journal of Symbolic Logic 48 (1983), no. 1, pp. 182–184, doi: 10.2307/2273332.
