# Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?

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?

• 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? – András Salamon May 29 '14 at 16:31
• 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? – hafeed May 29 '14 at 16:48
• 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/…? – Andrej Bauer May 30 '14 at 12:05
• 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. – hafeed May 30 '14 at 13:40

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.
• 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. – Emil Jeřábek May 30 '14 at 21:31
• 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. – cody May 30 '14 at 22:21