I was reading the Trakhtenbrot's theorem in https://en.m.wikipedia.org/wiki/Trakhtenbrot%27s_theorem, and there is something I cannot understand.
I have read that, for any Turing Machine M, it is possible to build a logic formula $\phi_M$ s.t. $\phi_M$ is finitely satisfiable if and only if M halts. The idea, as far as I have understood, is to obtain $\phi_M$ by:
(1) considering some predicates that enables to represent the configuration of $M$ at different execution times. For instance, using some predicates $T_0(s, t)$ and $T_1(s, t)$ to represent that at time $t$ the value contained in the position s of the machine tape is 0 or 1, respectively.
(2) impose the necessary logic conditions to ensure that these different configurations follows the Turing Machine program.
My doubt is the following: If M does not hold, it seems to me that, then, every model of $\phi_M$ would satisfy that "every configuration is followed by another one", which, I think, could be encoded in logics by something like this: $\psi_M = \forall_{s, t}( (T_0(s, t) \lor T_1(s, t)) \rightarrow (T_0(s, t+1) \lor T_1(s, t+1))$).
Thus, I am reaching to the (wrong) point where we can check if a Turing machine M does not halt by checking if some first-order formula $\phi_M \rightarrow \psi_M$ is a theorem. However, this is impossible, since by running M in parallel to some algorithm to check if $\phi_M \rightarrow \psi_M$ is a theorem, we would decide if M halts. Could you help me to identify where is the mistake, please?
If we had an infinite model which claims that some machine "halts" in an infinite number of steps, this model will have an infinite number of steps followed by a single "final" step, so that it isn't true that every step is followed by another one, even though the model is infinite.
More generally, the problem is that you are trying to find a way of expressing "the model is infinite" in a first-order way, and then letting that formula be $\psi_M$. But if you could express "the model is infinite" then, by taking negations, you could express "the model is finite". That is impossible in this case, by compactness. Because Turing machines can take an arbitrarily long time to halt, the models can be of arbitrarily large finite size. By compactness, if a formula has models of arbitrarily large finite size, it also has infinite models. So there is no way to capture "the model is finite" in this case, than thus no way to capture "the model is infinite".