Reverse Mathematics of Well-Founded Induction in Primitive Recursive Arithmetic

Question

I have another question about Primitive Recursive Arithmetic, and I'll borrow it's axiomatization from my other question Does the Deduction Theorem fail for Primitive Recursive Arithmetic?. Consider that definitions of the forms $\phi \mathrel{\leftrightarrow_\mathrm{df}} \psi$ and $a \mathrel{=_\mathrm{df}} b$ introduce, respectively, the implications $\phi \to \psi$ and $\psi \to \phi$, and the equation $a = b$, as proper axioms, as well as extend the language with the new symbols in the definiens (the LHS of the definition). Consider also the following definitions:

1. $1 \mathrel{=_\mathrm{df}} S(0)$
2. $\bot \mathrel{\leftrightarrow_\mathrm{df}} 0 = 1$
3. $(\forall x < 0)\phi(x) \mathrel{\leftrightarrow_\mathrm{df}} \bot$
4. $(\forall x < S(t))\phi(x) \mathrel{\leftrightarrow_\mathrm{df}} (\forall x < t)\phi \land \phi(t)$

In definition 4, $x$ is assumed to not occur free in $t$, so as to avoid defining formulas such as $(\forall x < S(x))\phi$, which would do away with bounded quantification. Furthermore, since my formulation of PRA lacks conjunction as a primitive connective, instead of defining it and laboriously proving its properties, we can, exceptionally for definition 4, introduce instead the three implications $(\forall x < S(t))\phi(x) \to (\forall x < t)\phi$, $(\forall x < S(t))\phi(x) \to \phi(t)$ and $(\forall x < t)\phi \to (\phi(t) \to (\forall x < S(t))\phi(x))$ as proper axioms. This is merely a technical detail and, or so I believe, it shouldn't affect the resolution of this question significantly.

Finally, consider the schema $((\forall x < t)\phi(x) \to \phi(t)) \to \phi(t)$, effectively expressing well-founded induction. Again, $x$ is assumed to not occur free in $t$. If PRA had universal quantifiers, this schema would be equivalent to the formula $(\forall y)(((\forall x < y)\phi(x) \to \phi(y)) \to \phi(y))$.

We can prove this schema from the primitive inference rule of induction (to infer $\phi(t)$ from $\phi(0)$ and $\phi(x) \to \phi(S(x))$), definitions 3 and 4, and some propositional logic. But is the reverse true? Can we do away with the induction inference rule, in PRA, by replacing it with this schema? I suppose that, to do so, one needs at least enough logic (to deal with bounded quantifiers) to have been developed, which would itself require the induction inference rule, and the system resulting from taking the results of this development as primitive would be very similar to the subsystems of first-order arithmetic.