Essentially, yes. An old result of Kleene [1], later strengthened by Craig and Vaught [2], shows that every recursively axiomatizable theory in first-order logic without identity, and every recursively axiomatizable theory in first-order logic with identity that has only infinite models, has a finitely axiomatized conservative extension. See also Mihály Makkai’s review, and Richard Zach’s summary.
Let me stress that the results above apply to the literal definition of conservative extension, i.e., we extend the language of $T$ by additional predicate or function symbols, and we demand that any sentence in the original language is provable in the extension iff it is provable in $T$. If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension.
But back to the standard definition. I’m assuming logic with identity from now on. What happens for theories that may also have finite models? First, [2] give the following characterization (they call condition 1 “f.a.${}^+$”, and condition 2 “s.f.a.${}^+$”):
Theorem. For any theory $T$ in a finite language, the following are equivalent:
- $T$ has a finitely axiomatized conservative extension.
- There exists a finitely axiomatized extension $T'\supseteq T$ such that every model of $T$ expands to a model of $T'$.
- $T$ is equivalent to a $\Sigma^1_1$ second-order sentence.
Following Dmytro Taranovsky’s comments, we have the following necessary condition (which is actually also mentioned in [2], referring to Scholz’s notion of spectrum instead of NP, which was only defined over a decade later):
Theorem. For any theory $T$ in a finite language, 1 implies 2:
- $T$ has a finitely axiomatized conservative extension.
- $T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Indeed, the truth of a fixed $\Sigma^1_1$ sentence in finite models can be checked in NP.
I haven’t verified the details, but I believe this is in fact a complete description:
Claim. For any theory $T$ in a finite language, the following are equivalent:
- $T$ has a finitely axiomatized conservative extension.
- $T$ is recursively axiomatizable, and the set of its finite models is recognizable in NP.
Proof sketch:
By Fagin’s theorem, there exists a $\Sigma^1_1$ sentence $\Phi$ equivalent to $T$ on finite models. Since infiniteness is also $\Sigma^1_1$-definable, we may assume that all infinite models satisfy $\Phi$.
By the results of [1,2], there exists a $\Sigma^1_1$ sentence $\Psi$ equivalent to $T$ on infinite models. I claim that $\Psi$ can be chosen so that it holds in all models of $T$, including finite (but it may also hold in other finite structures). Then $\Phi\land\Psi$ is a $\Sigma^1_1$ sentence equivalent to $T$ in all models, proving the result.
Now, to construct $\Psi$, [1,2] take a suitable finite fragment of arithmetic, enough to numerate a recursive axiomatization of $T$, and augment it with a kind of truth predicate for formulas in the language of $T$, with the postulate that all axioms of $T$ (as given by the numeration) are true (according to the truth predicate).
As is, this finite theory has no finite models at all. However, instead of usual arithmetic, we may use (a finite fragment of) the theory $\mathrm{PA^{top}}$: here, the function symbols $S,+,\cdot$ are replaced with predicates representing their graphs, and the axioms of the theory only make them partial functions; there is an axiom that there exists a maximal element, and we have the induction schema. Notice that since we have a largest element, all quantifiers are effectively bounded, even if not written that way; one can show that the models of $\mathrm{PA^{top}}$ are exactly the bounded intervals $[0,a]$ of models of $I\Delta_0$. (In particular, it has finite models $[0,n]$ of arbitrary size.)
Now, since the theory has roughly the strength of $I\Delta_0$, we may still numerate axioms of $T$ inside it. The numerating formula will be satisfied by (codes of) all standard axioms of $T$ in any infinite model, while in a finite model, it will be satisfied by a finite initial subset of the axioms (those that fit, along with all required witnesses, in the given model). Likewise, we may add a truth predicate, which will work as expected for all standard formulas in an infinite model, while in a finite model, it will only work for a finite initial subset of formulas. If we set it up properly, the truth predicate will work for all formulas that may be numerated in the given model. Thus, if we then postulate, as before, that all formulas from the numeration are made true by the truth predicate, this will imply all of $T$ in an infinite model, and it will amount to a finite subtheory of $T$ in a finite model. Either way, any model of $T$ then has an expansion to a model of the extended theory.
References:
[1] Stephen Cole Kleene: Finite axiomatizability of theories in the predicate calculus using additional predicate symbols, in: Two papers on the predicate calculus. Memoirs of the American Mathematical Society, no. 10, Providence, 1952 (reprinted 1967), pp. 27–68.
[2] William Craig and Robert L. Vaught: Finite axiomatizability using additional predicates, Journal of Symbolic Logic 23 (1958), no. 3, pp. 289–308.