I was reading the sketch of the proof of Tarski's theorem in Jech's "Set Theory", which appears as Theorem 12.7, thinking that it would be an interesting result to really understand. As stated in the book, it is essentially a syntactic result (after fixing a Gödel numbering). However, after reading other proofs of Tarski's result, and really delving into the sketched proof, I believe that there is a serious error in Jech's proof, and now I'm not sure the result holds at the syntactic level.

Here is the problem as I see it. In the second sentence of the proof the formulas are enumerated as $$\varphi_0,\varphi_1,\varphi_2,\ldots.$$ Now, this is an enumeration outside ZFC, so the subscripts are metamathematical numbers. But in the next formula, which reads, $$x\in \omega \land \neg T(\#(\varphi_x(x))),$$ the subscript $x$ on $\varphi$ is being treated as a formal natural number---an element of $\omega$.

If we have a model of set theory, where $\omega$ matches the metamathematical natural numbers, maybe we could make this formula work. My question is whether or not we can somehow avoid making such a strong assumption. If not, what's the easiest way to assert such a matching (say, without forcing an interpretation of all of ZFC, just of the natural number part)?