Suppose we have a classical arithmetical theory $\mathbf{R}$, at least as strong as Robinson arithmetic, with $\tau$ an extra dummy monadic predicate in its language $\mathcal{L}$. Suppose $\mathbf{R}$ only has modus ponens as an inference rule.
Let the variables of $\mathcal{L}$ be indexed by the natural numbers. For a formula $\epsilon$ in $\mathcal{L}$, let $\forall\epsilon$ be $\epsilon$ if there are no free variables in $\epsilon$, else $\forall\forall x_i\epsilon$ where $x_i$ is the free variable of $\epsilon$ with smallest index.
Let the axiomatization of $\mathbf{R}$ be such that all the axioms are of the form $\forall\zeta$ for some $\zeta$ in $\mathcal{L}$, so that $\mathbf{R}$ only has sentences as axioms.
Suppose $\mathbf{R}$ has, for example, the axioms $A^1 \ \forall\alpha$, $A^2 \ \forall\beta$ and $A^3 \ \forall\gamma$, and, to repeat, just modus ponens as inference rule.
Suppose [] is a Gödel-coding provided by $\mathbf{R}$.
May I define a system such as $\mathbf{T}$, in the following, by using axioms $A^{\tau1} \ \tau[\forall\alpha]$, $A^{\tau 2} \ \tau[\forall\beta]$, $A^{\tau 3} \ \tau[\forall\gamma]$, as well as $A^{\tau 4} \ \tau[\tau[\forall\forall x_i\eta(x_i)]\leftrightarrow\forall\forall x_i\tau[\eta(\dot{x_i})]]$ and $A^{\tau 5} \ \tau[\forall\delta]\to\forall\delta,$ and the inference rule $\vdash\tau[\forall\epsilon] \ \& \ \vdash\tau[\forall\epsilon\to\forall\zeta] \ \Rightarrow \ \vdash\tau[\forall\zeta]$? If not, why not?
