I've now asked this question on mathoverflow here.

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?

  • $\begingroup$ Good question. As an aside, does your statement that every theory with a finitely axiomatized conservative extension must be effectively axiomatizable have a more informative proof than arguing that the extended theory is r.e., hence the set of theorems in the unextended theory is r.e. and gives an r.e. axiomatization of itself, but r.e. axiomatizablility is equivalent to effectively axiomatizability? $\endgroup$
    – Rob Arthan
    Mar 20, 2019 at 21:01
  • $\begingroup$ @RobArthan The proof I had in mind was exactly the one you gave. $\endgroup$ Mar 20, 2019 at 21:31
  • $\begingroup$ I asked this on mathoverflow here. $\endgroup$ Mar 27, 2019 at 11:10
  • 1
    $\begingroup$ The same question asked at MathOverflow had an affirmative answer. $\endgroup$ Jul 11, 2019 at 8:57
  • $\begingroup$ I tried to post a CW answer that pointed to the answer you've got on MO, so there would be something to accept ... but the system thought it looked too trivial and converted it to a comment :-/ $\endgroup$ Jul 11, 2019 at 9:01

1 Answer 1


Emil Jeřábek answered of on mathoverflow.


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.*


*There is more than one way how to show this, but for example it follows immediately from the above mentioned result that any r.e. theory with only infinite models has a finite conservative extension: simply endow the given theory with a new sort (with no further structure), and axioms that make it infinite.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .