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

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?

• Can you give a concrete example of $\phi$? Jun 4 '20 at 13:36
• @AsafKaragila Let's assume that we have proven the correspondense between $\Delta_0$ formulas and Gödel operations(the Gödel normal form theorem). I'd like to see when $\phi(x)$ is "$x$ is in the Gödel closure of $\{V_\alpha: \alpha \in \mathrm{Ord}\}$. With the formula given, we can use the Reflection principle and reletivization freely, so I thought that it is convenient to leap to the metalanguage.
– Ris
Jun 4 '20 at 13:48

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.
• Thanks for your answer. Following your method $\psi$ is a fixed formula and works great. But can we also have $\psi$ vary over $x$? I mean, elevating the $\theta$ to a "real formula".
• You only make your life more difficult if you let the formula $\psi$ vary, so that works too. Just be careful that you cannot assume that the $\theta$ is a real formula immediately, (nonetheless it can be replaced by a real formula with the argument above). Jun 5 '20 at 10:29