I originally asked this question on math.stackexchange.com [here][1].

There's a famous theorem (due to Montague) that states that if $\sf ZFC$ is consistent then it cannot be finitely axiomatized. However $\sf NBG$ set theory is a conservative extension of $\sf ZFC$ that can be finitely axiomatized.

Similarly, if $\sf PA$ is consistent then it is not finitely axiomatizable (Ryll-Nardzewski) but it has a conservative extension, $\sf ACA_0$, which is finitely axiomatizable. (Usually $\sf ACA_0$ is considered a second-order theory, but my understanding is that there isn't really a difference between first and second-order from the syntactic point of view.)

I'm wondering if this happens in general. At first I thought it might be that every theory had a finitely axiomatizable conservative extension. But then I realised that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable. So we shouldn't hope for theories to have finitely axiomatizable conservative extensions unless they're already effectively axiomatizable. Similarly if we add countably many logical constants to the language and demand that they're all true then that's effectively axiomatizable but doesn't have a finitely axiomatizable conservative extension, so we should restrict our attention to finite languages.

Does every effectively axiomatizable first-order theory over a finite language have a finitely axiomatizable conservative extension? [1]: https://math.stackexchange.com/questions/3155201/does-every-effectively-axiomatizable-first-order-theory-have-a-finitely-axiomati