lo.logic – Is $mathsf{R}$ axiomatizable by finitely many schemes?

Recall that $mathsf{R}$ is the theory of arithmetic consisting of the quantifier-free theory of $(mathbb{N};+,times,0,1,<)$ together with, for each $kinmathbb{N}$, the sentence $$forall x((bigwedge_{i<k}xnot=underline{i})rightarrow underline{k}<x)$$ where $underline{n}$ is the numeral standing for $n$. $mathsf{R}$ is strong enough to be subject to the first incompleteness theorem, is pretty close to optimal in that sense (see here for some discussion of this point), and is not finitely axiomatizable (in contrast with Robinson’s more famous arithmetic $mathsf{Q}$).

My question is whether $mathsf{R}$ is finitely axiomatizable when we allow schemes, in a limited sense, as well as sentences. By “scheme” here I mean the following:

A scheme of sentences in a given language $Sigma$ is a sentence $sigma$ in the language gotten by adding a new relation symbol $R$ (of some finite arity) to $Sigma$. An instance of a scheme $sigma$ is then a sentence of the form $$forall y_1,…,y_n(sigma(R/varphi(y_1,…,y_n,x_1,….,x_k)))$$ where $varphi$ is some $(n+k)$-ary formula in the original language $Sigma$ and $sigma(R/varphi(y_1,…,y_n,x_1,…, x_k))$ is the $L$-formula gotten by replacing each “$R(t_1,…,t_k)$” with “$varphi(y_1,…,y_n,t_1,…,t_k)$” throughout $sigma$.

See here for some comments on this notion. A theory is scheme-finitely axiomatizable if it can be axiomatized by a finite set of sentences together with the set of all instances of finitely many schemes in the above sense. Clearly every scheme-finitely axiomatizable theory is computably axiomatizable, but the converse fails even for finite languages. I suspect that in fact $mathsf{R}$ witnesses the failure of the converse – basically, $mathsf{R}$ doesn’t seem to entail any nontrivial schemes in this particular sense at all – but I don’t see how to prove that.