Is "going through the metalanguage" while proving a theorem allowed?

Question

For instance, we want to prove that $\mathsf{ZFC} \vdash \forall x[x \in \mathrm{OD} \implies \phi(x)]$ for some formula $\phi(x)$ of the language of set theory ($\mathrm{OD}$ is the class of ordinal definable sets.) $\mathrm{OD}$ has two definitions which can be proved equivalent, the metalanguage version which quantifies the formulas directly, and the internalized version(Actually I'm not sure that this is right.) I am interested in using the former version to prove the theorem. Let $M$ be an arbitrary model of $\mathsf{ZFC}$. It suffices to prove that $\forall x \in M[M \vDash x \in \mathrm{OD} \implies M \vDash \phi(x)]$. We invoke here the equivalent metalanguage definition to get a formula $\psi$ and ordinals $\alpha_1, \ldots, \alpha_n \in M$ such that $$M \vDash \forall y[y \in x \iff \psi(y, \alpha_1, \ldots, \alpha_n)]$$ holds, and then prove $M \vDash \phi(x)$ with it. Is this a valid way to prove theorems?

Answer 1

Yes this is allright. Showing $\mathrm{ZFC}\vdash\forall x[x\in\mathrm{OD}\Rightarrow\phi(x)]$ is by Gödels completeness theorem equivalent to showing that the formula $\forall x[x\in\mathrm{OD}\Rightarrow\phi(x)]$ is true in any model $M$ of $\mathrm{ZFC}$. Now as you mention, if one picks an arbitrary such $M$, this amounts to showing $M\models\phi(x)$ for all $x\in\mathrm{OD}^M$. By definition of $\mathrm {OD}$, we have $$M\models \exists\theta\in\mathrm{Fml}\exists\alpha<\beta\forall y [y\in x\Leftrightarrow \mathrm{Sat}(V_\beta, \theta, y, \alpha)]$$

(note that one $\alpha$ is enough since $M$-finitely many ordinals can be coded into one) for such $x$. Now we can pick witnesses $\theta, \alpha, \beta$ for this statement (note that $\theta$ is essentially an $M$-integer, thus $M$-ordinal). This yields a real formula $\psi$ so that $$M\models\forall y\ y\in x\Leftrightarrow\psi(y, \theta,\beta,\alpha)$$ Now $x$ fits the bill for the kind of sets $z$ for which you have shown $M\models\phi(z)$ and thus $M\models\phi(x)$ as desired.