Ttyjfyk

I originally asked this question on math.stackexchange.com 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?

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:

1. 
   $T$ has a finitely axiomatized conservative extension.


2. There exists a finitely axiomatized extension $T'supseteq T$ such that every model of $T$ expands to a model of $T'$.


3. 
   $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:

1. 
   $T$ has a finitely axiomatized conservative extension.


2. 
   $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]