Proof of Trakhtenbrot's theorem

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.

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.

StackExchange Computer Science Q#11327, answer score: 6