Metamathematics of Kunen's proof of the Truth and Definability Lemmas

Question

I’m going through the forcing chapter in Kunen’s Set Theory (the 2011 edition) and I’m confused with some of the metatheoretic aspects of Kunen’s proof of the following:

Lemma (The Truth Lemma) Let $M$ be a countable transitive model (ctm) for ZF-P, let $\mathbb{P}\in M$ be a forcing poset, let $\psi$ be a sentence of $\mathcal{FL}_\mathbb{P}\cap M$ ($\mathcal{FL}_\mathbb{P}$ is the set of formulas in the language which has $\in$ as a binary relation and all $\mathbb{P}$-names as constant symbols), and let $G$ be a $\mathbb{P}$-generic filter over $M$. Then $M[G]\models \psi$ iff there is a $p\in G$ such that $p\Vdash \psi$.

Lemma (The Definability Lemma) Let $M$ be a ctm for ZF-P. Let $\varphi(x_1,\dots,x_n)$ be a formula in $\mathcal{L}=\{\in\}$, with all free variables shown. Then $$\left\{ (p,\mathbb{P},\le,\mathbb{1},\vartheta_1,\dots,\vartheta_n):(\mathbb{P},\le,\mathbb{1}) \text{ is a forcing poset} \wedge (\mathbb{P},\le,\mathbb{1})\in M\wedge \vartheta_1,\dots,\vartheta_n\in M^\mathbb{P} \wedge p\Vdash_{\mathbb{P},M}\varphi(\vartheta_1,\dots,\vartheta_n)\right\}$$ is in $\mathcal{D}^-(M)$ (the set of sets definable without parameters in $M$.

Now, since we are talking about set models, these results can be interpreted as single statements in ZFC (having developed logic and model theory within ZFC). Moreover, the author is in general careful to mention when some theorem is in fact a scheme in the meta theory, and does not say anything in regards to these two results.

When it comes to proving these lemmas, Kunen defines an auxiliary relation $\Vdash^*$, first for atomic sentences $\varphi\in \mathcal{AL}_\mathbb{P}$, and then for general sentences $\varphi$ of $\mathcal{FL}_\mathbb{P}$ by induction on the length of $\varphi$. In doing this, Kunen mentions that there is a logical technicality; for reasons related to Tarski’s undefinability of truth, the definition of $\Vdash^*$ must be carried out in the metatheory, and not within ZFC, since we would need to apply recursion to a proper class of objects. Thus, what we are really doing is assigning, in the metatheory, to teach formulas $\varphi(x_1,\dots,x_n)$ of $\mathcal{L}=\{\in\}$ with $n$ free variables another formula $Forces_\varphi(\mathbb{P},\le,\mathbb{1},p,\varkappa_1,\dots,\varkappa_n)$ with $n+4$ free variables asserting that $(\mathbb{P},\le,\mathbb{1})$ is a forcing poset, $p\in\mathbb{P}$, $\varkappa_1,\dots,\varkappa_n\in V^\mathbb{P}$ (there are no models here) and $p\Vdash^*_\mathbb{P}\varphi (\varkappa_1,\dots,\varkappa_n)$.

After this has been done, a series of results on the relation $\Vdash^*$ are stated and proven, and he mentions that these are actually schemes in the metatheory, saying that for each formula of $\{\in\}$, something is provable. These results are then applied to prove the Truth and Definability Lemmas, as stated above. My question is, why is this legitimate? We would like to prove a single statement of set theory, so we should offer just a single proof. But we are using lemma schemes in the proof, for which we are accordingly providing proof schemes. Is there a reason this does not break down, or is my entire reasoning flawed?

Answer 1

This comment of yours

since we would need to apply recursion to a proper class of objects

threw me off for a bit. That's not the issue Kunen has in mind. The real issue is that

$$ \Vdash^*_{\mathbb P} $$

is not a definable class in $\mathrm{ZFC}$ -- it is not definable by a single formula, i.e. there is no formula $\phi$ such that $$ \Vdash_{\mathbb P}^* = \{ (p, \lceil \psi \rceil, \dot \tau_0, \ldots, \dot \tau_n) \mid p \in \mathbb P \wedge \dot \tau_0, \ldots, \dot \tau_n \in V^{\mathbb P} \wedge \phi(\lceil\psi\rceil, \dot \tau_0, \ldots, \dot\tau_n) \} $$ and the issue, roughly speaking, is that $\phi$ would have to talk about a certain satisfaction relation of (Gödel-codes of) formulae of arbitrarily large complexity in the Lévy hierarchy -- something that even for the trivial forcing $\mathbb P = \{\mathbb 1 \}$ and without allowing parameters is provably impossible.

There are a couple of solutions to this dilemma. Consider, for example, for any $n < \omega$ the relation $$ \Vdash_{\mathbb P}^* \restriction \Sigma_n = \{ (p, \lceil \psi \rceil, \dot \tau_0, \ldots, \dot \tau_n) \in \Vdash^*_{\mathbb P} \mid \psi \in \Sigma_n \} $$ It turns out that this relation, for any given $n$, is definable -- say by the formula $\phi_n$. In our metatheory (where the enumeration $n \mapsto \phi_n$ exists) we can then stitch together all of these definitions to a pseudo-definition of $\Vdash^*_{\mathbb P}$ in the obvious way. Using this pseudo-definition, we could then prove the Truth and Definability Lemma in our metatheory. This is equivalent to proving the formal scheme that the Truth and Definabilty Lemma provably hold in $\mathrm{ZFC}$ for all restrictions $\Vdash^*_{\mathbb P} \restriction \Sigma_n$.