I was told to ask this question on mathoverflow. I asked on math stack exchange whether there is a computably axiomatizable theory that can't be axiomatized by a finite number of axiom schemas. I got an answer, but it was a theory in an infinite language. Now, I am asking whether there is an example in a finite language.
EDIT by non-OP: this is the above-mentioned MSE question, and this answer gives the definition of "scheme" being used.
Let me give an example of a theory that is computably axiomatizable but isn't axiomatizable by finitely many schemas.
Fix any finite signature $\Omega$ with equality. Further by finite $\Omega$-models I'll mean models encoded by binary strings in a natural way. Observe that for any $\Omega$-theory $T$ axiomatized by finitely many schemas the set of all finite models of $T$ is $\mathtt{co}\text{-}\mathtt{NP}$. And observe that given a finite $\Omega$-model $\mathfrak{M}$ we could effectively construct an $\Omega$-sentence $\chi_{\mathfrak{M}}$ such that for any $\Omega$-model $\mathfrak{N}$ we have $$\mathfrak{N}\models \chi_{\mathfrak{M}}\iff \mathfrak{N}\simeq\mathfrak{M}.$$ Consider arbitrary computable set of finite $\Omega$-models $A$ that is closed under isomorphisms and isn't $\mathtt{NP}$. Let $U_A$ be the theory axiomatized by sentences $\lnot\chi_{\mathfrak{M}}$ for $\mathfrak{M}\in A$. Clearly $U_A$ is computably axiomatizable. However, the set of finite models of $U_A$ is the complement of $A$ and thus isn't $\mathtt{co}\text{-}\mathtt{NP}$. Hence $U_A$ couldn't be axiomatized by finitely many schemas.
This answers complements Fedor Pakhamov's, who provided an example of a computable theory that is not axiomatizable by finitely many schemas.
Following up on the comment by Andreas Blass to the question: Vaught proved that if a theory $T$ is computable and has "a modicum of coding", then $T$ is axiomatizable by a scheme. Vaught's result was improved by Albert Visser, in the paper below, where "the modicum of coding" used by Vaught is reduced to the modest demand that $T$ interprets a non-surjective unordered pairing, where pairing need not be functional.
A. Visser, Vaught's theorem on axiomatizability by a scheme, The Bulletin of Symbolic Logic, vol. 18 (2012), pp. 382-402.
A preprint of Visser's paper can be found here.
There are a number of algebraic theories (in equational logic specifically, no predicate symbols besides equality) which are of finite type (so the language has only finitely many function symbols) but not finitely axiomatizable. Often one demonstrates this with an infinite sequence of structures for the language, but in some cases one can establish this linguistically.
A simple example involves work with hyperidentities (check out my arxiv preprint for details, 1408.something something). We posit the theory given by the hyperidentity F(F(x)) ideq F(F(F(x))), which is short hand for an equational theory that says every unary function term t in a language has its square equal its cube, or forall x t(t(x)) = t(t(t(x)).
If we choose a language with one binary function symbol, we get a finitely axiomatizable theory. I forget what happens with two unary function symbols. With three, you get a recursively axiomatizable theory which is not finitely axiomatizable. You show this by looking at the Thue Morse sequence and use square free fragments to build long terms and show long instances are not derivable from short instances of the axioms.
It gets real fun with more complicated hyperidentities and larger sets of function symbols. Check out the preprint for other families of examples.
Gerhard "Is The Question Computably Decidable?" Paseman, 2020.06.19.
