There exist sentences of first-order logic that are satisfiable and are satisfiable only by models of infinite size. However, all such sentences I can think of are satisfied by infinite models that can be generated by a non-terminating algorithm of a finite size.

For a example, there exists a sentence of first-order logic that is satisfied only by a model of an infinite size:

$$ \exists x \lnot \exists y S ( y, x ) \land $$ $$ \forall x \exists y S ( x, y ) \land $$ $$ \forall x \forall y \forall z ( ( S ( x, z ) \land S ( y, z) ) \to x = y ) $$

A model for this sentence can be generated (listed, enumerated) by a finite algorithm that never terminates - just list the elements of the infinite model in a sequence one after another and make $S$ hold only for successive pairs of such elements.

Does there exist a sentence of first-order logic that is satisfiable only in some infinite models for which there does not exist a finite algorithm that generates them?

  • 2
    $\begingroup$ A sentence is either true or false; formulas with free variables are the usual objects of interest for satisfiability. Do you mean a sentence which only has infinite models? If so, you seem to be asking for a sentence that is true only in non-computably enumerable models, and which is false in every c.e. language. It is also not clear what your logic is: are there any function or relational symbols, and if so, how are they interpreted? $\endgroup$ Commented May 29, 2014 at 16:31
  • $\begingroup$ Yes, I mean a sentence that is true only in non-computably enumerable models. The logic is first-order logic with equality, relational and functional symbols. Could you tell why such a sentence does not exist in any c.e. languages? $\endgroup$
    – hafeed
    Commented May 29, 2014 at 16:48
  • 1
    $\begingroup$ I do not understand the question. If the only task is to enumerate the elements of the model, that's easy: enumerate $\mathbb{N}$. Because, if the theory has only infinite models then it has a countably infinite model $M$, and there is a bijection between $M$ and $\mathbb{N}$, so we can transfer the model structure from $M$ to $\mathbb{N}$. Note that you are not allowed to say that the bijection $M \to \mathbb{N}$ is not computable until you explain what a computable model is. Maybe something like dagstuhl.de/Materials/Files/07/07441/…? $\endgroup$ Commented May 30, 2014 at 12:05
  • $\begingroup$ Andrej, thank you for the link to the slides. The task is not to enumerate the elements of the model, but to generate (list, enumerate) the whole model, which includes the interpretations of all relational and functional symbols. In my example there is a finite non-terminating algorithm that generates the model for the sentence, including an interpretation of the predicate $S$. I am asking, if there is a sentence that is true only in some infinite models that can not be generated by a finite non-terminating algorithm. $\endgroup$
    – hafeed
    Commented May 30, 2014 at 13:40

1 Answer 1


One possible answer to your question is Tennenbaum's Theorem. It states that no non-standard model of arithmetic can have only computable operations, i.e. either addition or multiplication will be non-computable given any recursive description of the elements of the model.

Now the remaining difficulty is having a single formula which has as models only non-standard models of arithmetic. Note that while arithmetic isn't finitely axiomatizable, there are conservative extensions of PA which are finite.

Now it's easy to build an infinite axiomatization of (an extension of) PA which has only non-standard models: add to PA a constant $c$ and the axioms $$ c\neq 0,\ c\neq S(0),\ c\neq S(S(0)),\ldots$$

There's a trick to turn this into a finite axiom. Add the binary predicate $\mathrm{NS}$ to your language, along with the axiom $$ \forall xy,\ \mathrm{NS}(x, y)\leftrightarrow x\neq y\wedge \mathrm{NS}(x, S(y))$$ Then the above schema is expressed by $\mathrm{NS}(c, 0)$.

Important edit: It is crucial that the induction schema (as axiomatized by your finite theory) does not apply to formulas containing $\mathrm{NC}$! Otherwise it is quite easy to show $\forall y,\ c\neq y$ and conclude $c\neq c$, a contradiction. I think that if you exclude those formulas from the induction principle, the above reasoning should go through without trouble.

  • 3
    $\begingroup$ Instead of extending an already very strong theory, you can take a weak finite subtheory: Tennenbaum’s theorem holds for just about any fragment of induction that allows formulas with some quantifiers (such as $IE_1$ and above), and plenty of such theories are finitely axiomatizable. Also, instead of the NS business, you can just throw in any consistent but unsound axiom. $\endgroup$ Commented May 30, 2014 at 21:31
  • $\begingroup$ Yes that's indeed much simpler thanks! I guess the power of a theory is in the eye of the beholder... Set theorists tend to think ZFC+ there are $\omega$ inaccessible cardinals is weak. $\endgroup$
    – cody
    Commented May 30, 2014 at 22:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.