34
$\begingroup$

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?

Improve this question
$\endgroup$
8
  • 1
    $\begingroup$ I suspect the answer is yes via some modified form of $\sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory. $\endgroup$
    – James E Hanson
    Commented Mar 27, 2019 at 11:28
  • $\begingroup$ The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $\sf NGB$ to get a finitely axiomatizable theory. $\endgroup$
    – James E Hanson
    Commented Mar 27, 2019 at 11:31
  • 1
    $\begingroup$ @JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M \vDash T$ where $\vDash$ and $T$ are interpreted in their natural way in the larger theory. [...] $\endgroup$
    – François G. Dorais
    Commented Mar 27, 2019 at 12:13
  • $\begingroup$ [...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $\operatorname{Con}(T)$ there is no reason for $M \vDash \operatorname{Con}(T)$ to be true. This is probably not what Oscar really wants... $\endgroup$
    – François G. Dorais
    Commented Mar 27, 2019 at 12:16
  • 1
    $\begingroup$ @OscarCunningham It's perfectly possible to write down a sentence in, say, $\sf ZFC$ that means $M \models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$. $\endgroup$
    – James E Hanson
    Commented Mar 27, 2019 at 15:25

1 Answer 1

Reset to default
29
$\begingroup$

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]

Improve this answer
$\endgroup$
12
  • $\begingroup$ @DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $\Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it. $\endgroup$
    – Emil Jeřábek
    Commented Mar 27, 2019 at 16:15
  • $\begingroup$ Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types. $\endgroup$
    – Dmytro Taranovsky
    Commented Mar 27, 2019 at 16:45
  • $\begingroup$ Yes, for finite models, being in NP is the same as being $\Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $\Sigma^1_1$ sentence $\Phi$ such that $M\models T\iff M\models\Phi$ for finite models $M$. By the results above, there is also a $\Sigma^1_1$ sentence $\Psi$ such that $M\models T\iff M\models\Psi$ for infinite models $M$. We may actually assume that $\Psi$ has no finite models, as infiniteness is $\Sigma^1_1$. However, finiteness is not $\Sigma^1_1$, hence we have no information ... $\endgroup$
    – Emil Jeřábek
    Commented Mar 27, 2019 at 17:07
  • 1
    $\begingroup$ It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4). $\endgroup$
    – Fedor Pakhomov
    Commented Mar 29, 2019 at 5:51
  • 1
    $\begingroup$ @OscarCunningham 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. (Or, to present it differently, relativize the original theory to a new unary predicate, and include axioms that make the domain infinite.) Then apply the original result. $\endgroup$
    – Emil Jeřábek
    Commented Dec 2, 2019 at 12:17

You must log in to answer this question.

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