(Un)Decidability of satisfiable but not finitely-satisfiable formulas

I am curios about the decidability or undecidability of the following decision problem.

INPUT: a first-order formula $\varphi$

OUTPUT:

• Yes, if $\varphi$ is satisfiable but not finitely-satisfiable

• No, otherwise

The problem is very close to Church's and Trakhtenbrot's Theorems, but somehow I do not see how to modify the proof of these two results in order to get the undecidability of this other result.

Somehow what I am asking corresponds to the fact of whether it is decidable or undecidable the problem of "deciding the finite model property".

Does anybody know whether the problem is undecidable or not? Does anybody know any reference where this is discussed?

• What does "finitely satisfiable" mean? – Cheerful Parsnip Jan 21 '11 at 23:05
• It means satisfiable in a finite structure (i.e., with finite domain). – boumol Jan 21 '11 at 23:10

The question is not decidable, since the halting problem reduces to it.

Suppose that we are given a Turing machine $M$ and we want to determine whether it halts on input 0. A halting computation can be described as a finite sequence of finite TM configurations, such that the initial configuration shows the appropriate set-up for M and each step of the configuration follows the computational rules specified by M and the final configuration shows the machine in a halting configuration. These properties of such a sequence of configurations can be described in a single statement $\varphi$, using a language enabling us to speak of cells of the tape and their contents and the head position of a given configuration and so on.

Thus, M halts if and only if $\varphi$ has a finite model.

Finally, we can arrange the details so that $\varphi$ trivially has an infinite model. Let us suppose that $\varphi$ describes the configurations in such a way that once the machine has halted, we can simply repeat the halting configuration at the next stage. That is, $\varphi$ should assert that the successor steps of computation work correctly, if the computation has not yet halted, but if it has, then the next configuration just copies the previous one as an exact duplicate. Now, if M does not halt, we can generate an infinite sequence of configurations corresponding to that, and then add another $\mathbb{Z}$-block of configurations all the same, showing a (fake) halting configuration. This will be an infinite model of $\varphi$.

Thus, for this $\varphi$, we see that $M$ halts if and only if the answer to your inquiry is no. So your inquiry is not asking a decidable question.

• I think your proof do not work. What you have showed is that $M$ halts iff the formula $\varphi$ is finitely and infinitely satifiable – boumol Jan 22 '11 at 0:39
• If M halts, then $\varphi$ is finitely satisfiable, so the answer is no. If the answer is no, then $\varphi$ is either not satisfiable or is finitely satisfiable. But since I argued that $\varphi$ is (infinitely) satisfiable in any case, then this means that no implies $\varphi$ is finitely satisfiable, and so M halts. – JDH Jan 22 '11 at 0:46
• Now I see your point. First of all you claim that 1. $M$ halts if and only if $\varphi_M$ has a finite model. 2. For every $M$, $\varphi_M$ has an infinite model. From these two facts it is clear that it follows that 3. $M$ does not halt if and only if $\varphi_M$ has a model but not a finite one. Do you any textbook or paper where this could be written as a numbered result? – boumol Jan 22 '11 at 1:15
• Yes, that's right. But I'm sorry that I don't know of any text with an argument like this. I am sure that there are simpler examples. I guess you can also just reduce the finite model property to your problem in the same way: if you want to determine whether $\psi$ has a finite model, then ask your question about $\psi\vee\theta$, where $\theta$ is satisfiable but only in infinite models. – JDH Jan 22 '11 at 10:25
• Comment deleted (there was a mistake) – boumol Jan 23 '11 at 11:25