Formulation of constructible power in terms of Gödel operations; Going through metatheory

Question

I am studying with Jech's Set Theory. He states this:

For every transitive set $M$, $$\operatorname{def}(M) = \operatorname{cl}(M \cup \{M\}) \cap \mathcal{P}(M)$$ where $\operatorname{cl}$ denotes the closure under Gödel operations.

He proves $\operatorname{def}(M) \supset \operatorname{cl}(M \cup \{M\}) \cap \mathcal{P}(M)$ like this: Let $X \subset M$ and $G$ be a (composite of) Gödel operation(s) such that $X = G(M, a_1, a_2, \ldots, a_n)$ where $a_1, \ldots, a_n \in M$. We have proven that if $G$ is a Gödel operation there is a $\Delta_0$ formula $\phi$(!) such that for all $M, a_1, \ldots, a_n$, $G(M, a_1, \ldots, a_n) = \{x \mid \phi(M, x, a_1, \ldots, a_n)\}$. So by altering all bounded quantifiers $(\exists v_m \in M)$ to $(\exists v_m)$ in $\phi$ and denoting the result as $\psi$, $X = \{x \in M \mid M \vDash \psi(x, a_1, \ldots, a_n)\}$ so $X \in \operatorname{def}(M)$.

These are my thoughts on the proof: Let $\mathsf{LST}$ be the language of set theory, and $\mathcal{L}$ be the formal counterpart of $\mathsf{LST}$ in $\mathsf{ZF}$. At the point (!), if $\phi$ is a $\mathsf{LST}$ formula, we can't do something like "for $G$ there exists $\phi$ s.t. ..." because we are proving in $\mathsf{ZF}$. However the satisfaction relation for $\Delta_0$ formulas $\vDash_0$ can be formalized in $\mathsf{ZF}$, i.e. there is a $\mathsf{LST}$ formula $\vDash_0$ such that for all $\Delta_0$ $\mathsf{LST}$ formula $\phi$, if $\phi'$ is the formal counterpart of $\phi$ in $\mathcal{L}$, $(\forall\overline{x})[\phi(\overline{x}) \leftrightarrow \vDash_0 \phi'(\overline{x})]$. Indeed this is a metatheorem. So (!) can and should be implemented by the formal counterpart. Are my thoughts correct?

Answer 1

What you've outlined works. However, it's worth noting that we can dodge Godel operations altogether: the full satisfaction relation for set-sized structures can be directly treated in ZFC.

To my mind the most intuitive approach is via Skolem functions. Roughly speaking, $\mathcal{A}\models\varphi$ iff there is a family of functions from Cartesian powers of $\mathcal{A}$ to $\mathcal{A}$ which serve as a family of Skolem functions for $\varphi$ in $\mathcal{A}$.

If you want to avoid Skolem functions, you can also talk about syntax trees. Roughly speaking, we assign to a sentence $\varphi$ in a structure $\mathcal{A}$ a tree $T$ whose nodes are subformulas of $\varphi$ with free variables replaced by elements of $\mathcal{A}$ (e.g. the root is $\psi$, a node $\forall x(\psi(x))$ will have as successors each sentence $\psi(a)$ for $a\in\mathcal{A}$, etc.). We say $\mathcal{A}\models\varphi$ iff there is a subtree $S\subseteq T$ satisfying some basic properties (e.g. $\varphi\in S$, if $\theta\vee\psi\in S$ then $\theta\in S$ or $\psi\in S$, if $\forall x\psi(x)$ is in $S$ then for each $a$ the sentence $\varphi(a)$ is in $S$, etc.).

Each of these definitions (and various others) works appropriately in ZFC. The key point here is that we assume that $\mathcal{A}$ is a set, and so the collection of functions on $\mathcal{A}$ or appropriate trees is in fact something we can talk about. If we try to apply this idea to $V$ we find ourselves needing to quantify over functions from $V$ to $V$ (or morally equivalent objects), which we can't do. So that's why this doesn't break Tarski's undefinability theorem.

Answer 2

I'll add the following:

The way Jech states the Gödel Normal Form Theorem, it looks like a scheme in the metatheory, since "operations" are classes, and it seems to be quantifying over classes.

There is also a way around this, in the sense that we can write a single formula $\Phi(x,y)$ in the LST which says "$y$ is obtained from $x$ by Gödel operations". Indeed, let $\Psi_i(u,v)$, for $i<10$, be formulas defining each of the basic Gödel operations. Then $\Phi(x,y)$ is the formula $$ \exists n\in\omega \exists z \left[\text{seq}(z,n) \wedge x=z(0) \wedge y=z(n)\wedge \forall j<n \bigvee_{i<10} \Psi_i (z(i),z(i+1))\right] $$ where $\text{seq}(u,v)$ is a formula in LST which says that $u$ is a function with domain $v\cup \{v\}$.

The key here was that the "there exists" clause of the (meta)theorem referred to some fixed formulas, so you can just go ahead and list them. This makes the statement longer, of course.

As an additional point, quantifying over formulas is not in itself a problem, as LST formulas are readily formalized as objects in $HF$, and you can write a very-absolute LST formula $Fml(v)$ which says "$v$ is a (formal) formula in $\mathcal{L}$" . Things get dicey when you want to say "$\phi$ is true" in a class as a property of the formal object $\phi$. For set sized structures, this can be avoided as mentioned by Noah Schweber.

I find Devlin's Constructibility to be very clear in all these LST vs $\mathcal{L}$ matters (in fact, that's the exact notation he uses, so you might have already taken a look at it). There are some well-known issues with in the first chapter, which are fixed in a paper by Mathias, and have to do with the exact weak fragment of $ZFC$ he's using.