(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?
 A: 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.
