3
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ Can you give a concrete example of $\phi$? $\endgroup$
    – Asaf Karagila
    Jun 4 '20 at 13:36
  • $\begingroup$ @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. $\endgroup$
    – Ris
    Jun 4 '20 at 13:48
2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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". $\endgroup$
    – Ris
    Jun 5 '20 at 9:49
  • $\begingroup$ 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). $\endgroup$ Jun 5 '20 at 10:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.