Is $\mathsf{R}$ axiomatizable by finitely many schemes?

Question

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 $k\in\mathbb{N}$, the sentence $$\forall x[(\bigwedge_{i\le k}x\not=\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 (see Beklemishev and Jerabek for some relevant information on 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 $A$ (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[A/\varphi(y_1,...,y_n,x_1,....,x_k)])$$ where $\varphi$ is some $(n+k)$-ary formula in the original language $\Sigma$ and $\sigma[A/\varphi(y_1,...,y_n,x_1,..., x_k)]$ is the $L$-formula gotten by replacing each "$A(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. Separately, I don't believe that the Visser/Vaught result on axiomatization by schemes can give a positive answer here, since $\mathsf{R}$ seems to lack the needed coding power.

Answer 1

This answer is merely an advancement on the original question rather than a full answer.

Recall that a theory is locally finitely satisfiable if all its finite subtheories have finite models. Below I sketch a proof of the following theorem.

Theorem. There exists an extension $\mathsf{U}$ of $\mathsf{R}$ that is axiomatized by finitely many schemes such that the assumption $\mathtt{PH}\ne\mathtt{ExpTime}$ implies that $\mathsf{U}$ is locally finitely satisfiable.

Note that there is a result of Visser [1] that $\mathsf{R}$ interprets any locally finitely satisfiable theory. Thus the theorem above implies that if $\mathtt{PH}\ne\mathtt{ExpTime}$, then there is a locally finitely satisfiable theory that is mutually interpretable with $\mathsf{R}$.

Proof. Let us fix a theory $\mathsf{U}_0$ axiomatized by finitely many schemes such that all its infinite models are models of $\mathsf{R}$ and its finite models are precisely the rings $\mathbb{Z}_{2^n}$ (the order in $\mathbb{Z}_{2^n}$ is the standard order on the set $\{0,1,\ldots,2^n-1\}$).

We identify elements of $\mathbb{Z}_{2^n}$ with the binary strings of the length $n$, where each number corresponds to its own binary expansion. For formulas $\varphi(x)$ we consider the languages $$D_\varphi=\{\alpha\mid \mathbb{Z}_{2^{|\alpha|}}\models\varphi(\alpha)\}.$$ If $\varphi(x)$ is a first-order arithmetical formula, then clearly $D_\varphi\in\texttt{PH}$. Observe that $$\{D_\varphi\mid \varphi(x)\in \Sigma^1_1\}=\bigcup_{k\in\omega} \mathtt{NTime}(2^{xk}),$$ where in $\Sigma^1_1$-formulas we allow quantification over predicates of any finite arity.

Fix an $\mathtt{ExpTime}$-complete language $L$ such that $L\in \mathtt{Time}(2^{xk})$, for some $k$. Clearly, $L,\bar{L}\in \mathtt{NTime}(2^{xk'})$, for some $k'$. Fix $\Sigma^1_1$-formulas $\varphi_0(x)$ and $\varphi_1(x)$ such that $S_{\varphi_0}=L$ and $S_{\varphi_0}=\bar L$. For $i\in\{0,1\}$ the formula $\varphi_i(x)$ is of the form $\exists X^{(n_i)} \psi_i(x,X^{(n_i)})$. Let $U$ be the extension of $U_0$ by the scheme $$\exists x (\lnot \psi_0(x,X^{(n_0+1)}\upharpoonright x)\land \lnot \psi_1(x,Y^{(n_1+1)}\upharpoonright x)),$$ where $X^{(n+1)}\upharpoonright x$ is the $n$-ary relation $\{(y_1,\ldots,y_n)\mid (x,y_1,\ldots,y_n)\in X^{(n+1)}\}$.

Observe that $U$ doesn't have finite models. Indeed any model $\mathbb{Z}_{2^n}$ clearly satisfies the $\Sigma^1_1$-sentence corresponding to the negation of the scheme above: $$\exists X^{(n_0+1)}, Y^{(n_1+1)}\forall x ( \psi_0(x,X^{(n_0+1)}\upharpoonright x)\lor \psi_1(x,Y^{(n_1+1)}\upharpoonright x)).$$ Thus for any $n$ we could construct an instance of the scheme that would fail in $\mathbb{Z}_{2^n}$.

To finish the proof we use the assumption $\mathtt{PH}\ne \mathtt{ExpTime}$ to show that any finite fragment of $U$ has a finite model. Otherwise there would be $N$ and fisrt-order formulas $\theta_{i,j}(x,y_1,\ldots,y_{n_j},\vec{p}_i)$, $0\le i<N$, and $j\in\{0,1\}$ such that $$\mathbb{Z}_{2^n}\models \bigvee\limits_{0\le i<N}\exists \vec{p}_i\forall x (\bigvee_{j\in\{0,1\}} \psi_j(x,\{(y_1,\ldots,y_{n_j})\mid \theta_{i,j}(x,y_1,\ldots,y_{n_j})\})).$$ But in fact this implies that $L$ is equal to $D_\eta$, where $\eta(x)$ is $$\bigvee\limits_{0\le i<N}\exists \vec{p}_i(\psi_0(x,\{(y_1,\ldots,y_{n_0})\mid \theta_{i,0}(x,y_1,\ldots,y_{n_0})\})).$$ Thus $L\in\mathtt{PH}$, contradicting the assumption that $\mathtt{PH}\ne\mathtt{ExpTime}$. QED

[1] Visser, A. "Why the theory R is special." Logic Group preprint series 279 (2009).