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, Richard Zach’s summary, and a related paper by Pakhomov and Visser [3].
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.
It is not known if this is a complete characterization: if $T$ is a r.e. theory whose finite models are NP, then $T$ is equivalent to a $\Sigma^1_1$ sentence on infinite models by [1,2], and $T$ is equivalent to a $\Sigma^1_1$ sentence on finite models by Fagin’s theorem, but it is unclear how to combine the two to a single $\Sigma^1_1$ sentence that works for all models. This is mentioned as an open problem in the recent paper [3].
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.
[3] Fedor Pakhomov and Albert Visser, On a question of Krajewski’s, Journal of Symbolic Logic 84 (2019), no. 1, pp. 343–358. arXiv: 1712.01713 [math.LO]