A homework(ish) problem from models of set theory:
Define $\varphi(x) :\leftrightarrow Lim(x) \land \forall y\in x \, (Lim(y)\rightarrow y=0)$ where $Lim(x)$ means that $x$ is a limit ordinal. $\varphi$ says that $x=\omega$. I can prove that $\varphi(x)$ is a definite formula : For any transitive model $M\subseteq V$ of $ZF$ and $x\in M$, $\varphi(x)$ is true iff the relativation $\varphi(x)^M$ is true. (because all quantifiers used in the definition of $\varphi(x)$ are bounded)
Now, being asked to prove that the term $\omega= \bigcap \{ x \, |\, Ind(x) \,\}$ is definite (where $Ind(x)\leftrightarrow 0\in x\land \forall y\in x : y\cup \{y\}\in x$), I want to argue as follows.
ZF proves $\exists x \varphi(x)$ and $\forall x (\varphi (x) \leftrightarrow x=\omega)$. So for a model $M$ of ZF, the relativations $\exists x\in M \varphi(x)$ and $\forall x\in M (\varphi(x)\leftrightarrow x=\omega^M)$ should be true. The first relativation implies $\omega\in M$ and the second implies $\omega^M=\omega$.
I have seen a proof that $\omega^M=\omega$ (for transitive models M of ZF) using a more direct argument, but is this also correct?
Your proof is essentially right. Someone might object that, where you wrote "So for a model $M$ of ZF, the relativations $\dots$ should be true," you should write the actual relativizations, which involve $\varphi^M$, and then invoke the first paragraph of your question to replace $\varphi^M$ with $\varphi$. But this is just a question of how much detail to include.
As long as people are pointing out in the comments that it is customary not to call $0$ a limit ordinal, I might as well also point out the usual terminology "relativizations" (instead of "relativations") and "absolute" (instead of "definite").