4
$\begingroup$

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?

  • 0
    What does "finitely satisfiable" mean?2011-01-21
  • 0
    It means satisfiable in a finite structure (i.e., with finite domain).2011-01-21

1 Answers 1

2

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.

  • 0
    I think your proof do not work. What you have showed is that $M$ halts iff the formula $\varphi$ is finitely and infinitely satifiable2011-01-22
  • 0
    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.2011-01-22
  • 0
    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?2011-01-22
  • 0
    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.2011-01-22
  • 0
    Comment deleted (there was a mistake)2011-01-23
  • 0
    Following last remark (in previous comment) by JDH there is a much simpler proof of the undecidability. Let us fix a formula $\theta$ which is satisfiable, but not finitely satisfiable. Then, the following two conditions are equivalent: (1) $\varphi$ is not finitely satisfiable, (2) $\varphi \lor \theta$ is satisfiable but not finitely-satisfiable. From Trakhtenbrot's Theorem we conclude that the problem considered in this question is undecidable.2011-01-23
  • 0
    Yes, that's right. But another perspective is that the reason that you know that the finite satisfiability problem is undecidable is by coding the halting problem, and so this argument ultimately unwinds to become the same argument I gave above.2011-01-24