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?

  • $\begingroup$ Can you give a precise reference to the spot where he talks about this metatheoretical skirmish? I'm asking because you can avoid all of that, if you restrict yourself to countable transitive models. And since Kunen takes this approach in his book, I'm surprised to hear that this issue even comes up. $\endgroup$ Dec 21, 2017 at 11:40
  • $\begingroup$ @StefanMesken will a page number suffice? Its page 260 in the 2011 edition. If not, I can upload the page in question. $\endgroup$
    – Reveillark
    Dec 21, 2017 at 13:05
  • $\begingroup$ Yep, that is sufficient. $\endgroup$ Dec 21, 2017 at 13:18

1 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$.

  • $\begingroup$ My comment pointed to the fact that the “obvious” definition of $\Vdash^*$ fails because the relation we’d like to induct on is non set-like. I’m q bit confused by the last statement, are the truth and definability lemmas actually schemes in the metatheory? Is it wrong to think of them as single statements of set theory? $\endgroup$
    – Reveillark
    Dec 21, 2017 at 18:23
  • $\begingroup$ You can rearrange the recursion on $\Vdash^*$ (restriction to names of bounded rank). What you can't do, is to handle all Gödel-codes uniformly, i.e. with a single statement. That being said, as far as the theory of forcing goes, it's fairly safe to pretend that these lemmas are single statements. In any given proof you only deal with finitely many formulae anyways and for those finitely many formulae (or more generally formulae of bounded complexity) you do have these lemmas as theorems of $\mathrm{ZFC}$. $\endgroup$ Dec 21, 2017 at 19:24
  • $\begingroup$ Sorry to be a bother, but I'm still a bit confused, what do you mean by "it's fairly safe to pretend [...] statements"?. Also, if we have a transitive set model $M$ and relativize the notion $\Vdash^*$ to $M$ (which would include considering only those formulas in the model $M$), wouldn't this be definable over $M$? Kunen says something along these lines in page 262, when he actually proves the Lemmas. $\endgroup$
    – Reveillark
    Dec 22, 2017 at 21:41
  • $\begingroup$ 1. part. It's not true that they are single statements in $\mathrm{ZFC}$ but you will likely not run into any trouble if you pretend like this was the case. That's what I mean. 2. part. $\Vdash^*$ relativized to $M$ is definable over $M$ in our background universe. But it is not a definable class in $M$. However, that's what we need. We need that $M$ itself knows $\Vdash^*$ (or at least $\Vdash^* \restriction\Sigma_n$ for all $n < \omega$) to make the proof of the forcing theorem work. $\endgroup$ Dec 23, 2017 at 0:49
  • $\begingroup$ Ok, I'll still have to think about it some more, but your comments have been very useful. Thank you very much for your help! :) $\endgroup$
    – Reveillark
    Dec 23, 2017 at 1:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .