Consider the following iteration of Primitive Recursive Arithmetic. Its primitive rules of inference are modus ponens (to infer $\psi$ from $\phi \to \psi$ and $\phi$) and induction (to infer $\phi(t)$ from $\phi(0)$ and $\phi(x) \to \phi(S(x))$). Its logical axioms are as follows:
- $\phi \to (\psi \to \phi)$
- $(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi))$
- $t = t$
- $s = t \to (\phi(s,s) \to \phi(s,t))$
In axiom 4, $\phi(s,t)$ is the result of substituting $t$ for at least one instance of $s$ in $\phi(s,s)$, as usual. Its proper axioms are the primitive recursive definitions of each primitive recursive function; for instance, the proper axioms for $+$ are $t + 0 = t$ and $s + S(t) = S(s + t)$. In both the logical and proper axioms, metavariables for formulas and terms have been used in order to do away with unnecessary variable substitution rules (such as: to infer $\phi(t)$ from $\phi(x)$).
My question is as in the title: does the Deduction Theorem fail for Primitive Recursive Arithmetic, and in particular this formulation of it? I know we can prove a restricted version, where we pass from $\Gamma, \phi \vdash \psi$ to $\Gamma \vdash \phi \to \psi$ only if the proof of $\Gamma, \phi \vdash \psi$ does not use the induction rule. But is there a way to prove the general Deduction Theorem, despite this rule?