Proof of Trakhtenbrot's theorem

Question

In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ such that $\Phi_M$ is finitely satisfiable iff $M$ halts on the empty input. Then he says that as the latter is known to be undecidable so the theorem holds.

My doubt is, the vocabulary $\sigma$ that was constructed depends on the Turing Machine $M$. But the theorem holds for any relational vocabulary with at least one binary relation symbol and also it should not depend on the machine $M$. Perhaps the claim of author is enough to imply the theorem for arbitrary vocabulary, but I am unable to see how.

Answer 1

I'm a bit late, but the only answer does not address the question.

You state that the vocabulary $\sigma$ depends on the choice of turing machine $M$. If this were the case, then indeed the claim would only follow for arbitrary vocabularies. But - as the index of $\Phi_M$ and the missing one of $\sigma$ hint at - only the formula depends on $M$, the vocabulary is fixed for all turing machines.

Now all this shows, is undecidability for this particular vocabulary $\sigma$. To get the desired undecidability for all vocabularies with at least one binary relation, we have to do the reduction using only a single binary relation. We do this by encoding all of $\sigma$ into a single binary relation. The specifics are a popular exercise (and indeed the first exercise in the chapter), and go back to techniques first used by Kálmar.

Answer 2

They perform a reduction: given an arbitrary Turing machine, they construct a specific formula equivalent to the question "Does this machine halt on $\varepsilon$?". If validity could be decided in the target logic, so could the halting problem, which contradicts its undecidability.

So yes, the formula can depend on the machine as much as it wants. See here to read more about this, and browse reductions questions for more examples.