<p>One possible answer to your question is <a href="http://en.wikipedia.org/wiki/Tennenbaum%27s_theorem">Tennenbaum's Theorem</a>. It states that no <em>non-standard</em> 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.</p>

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

<p>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$$</p>

<p>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)$.</p>

<p><strong>Important edit</strong>: 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. </p>

CC BY-SA 3.0
2014-05-30T21:31:27.063Z
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
CC BY-SA 3.0
2014-05-30T22:21:39.060Z
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
CC BY-SA 3.0
2014-05-30T15:29:56.770Z
2014-05-30T15:36:41.707Z
2014-05-30T15:36:41.707Z
cody
<p>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.</p>

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

<p>$$ \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 ) $$</p>

<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2014-05-29T16:31:32.957Z
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
CC BY-SA 3.0
2014-05-29T16:48:51.500Z
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
CC BY-SA 3.0
2014-05-30T12:05:24.163Z
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 http://www.dagstuhl.de/Materials/Files/07/07441/07441.HirschfeldtDenis.Slides.pdf?
Andrej Bauer
CC BY-SA 3.0
2014-05-30T13:40:55.657Z
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
<lo.logic>
Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?
hafeed
# Does there exist a sentence of first-order logic that is satisfiable only in infinite models that do not have a finite algorithmic representation?

(Asked by: username_0 on 2014-05-29)

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?

**Tags:** lo.logic
> **Comments:**
> **username_1**: 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?  
> **username_0**: 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?  
> **username_2**: 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 http://www.dagstuhl.de/Materials/Files/07/07441/07441.HirschfeldtDenis.Slides.pdf?  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_3 on 2014-05-30. Score: 9 | Accepted answer

One possible answer to your question is [Tennenbaum's Theorem](http://en.wikipedia.org/wiki/Tennenbaum%27s_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.

> **Comments:**
> **username_4**: 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.  
> **username_3**: 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.  

---

