Complexity of $\Vdash_{\mathbb{P}}$ when $\mathbb{P}$ is a class definable iteration

Question

Let $\mathbb{P}$ some class forcing iteration which is absolute enough. For instance, suppose that $\mathbb{P}$ is a $\Delta_1$-definable class iteration. Normally, this is the case for iteration of standard forcings like Cohen, collapses and so on. My question is basically technical and its related with the degree of complexity of the forcing relation $\Vdash_{\mathbb{P}}$. It is well-known that for set forcing notions $\mathbb{P}$ the forcing relation $\Vdash_{\mathbb{P}}$ for $\Sigma_n$-formulae ($n\geq 1$) is $\Sigma_n$-definable with $\mathbb{P}$ as a parameter. On the contrary, if $\mathbb{P}$ is a class this is not clear at all. Notice that in this context the quantifiers over conditions are unbounded so probably the complexity increases.

My question is the following:

Question: If $\mathbb{P}$ is a $\Delta_1$-definable class forcing iteration (suppose if you like that the iterates are Cohen forcings of whatever standard), then the forcing relation $\Vdash_{\mathbb{P}}$ for $\Sigma_n$-formulae is also $\Sigma_n$-definable? If not, could you give a bound for its complexity?

Thanks for your help!

Answer 1

There are several technical subtleties to consider when we try to define the forcing relation $\Vdash$ in the context of class forcing. First we need to distinguish between definable class forcing, i.e. in the context of $ZFC$-set theory and class forcing in the context of $KM$-set theory. Next for definable class forcing, there is the issue that the forcing relation $\Vdash$ might not even be definable in the ground model $M$. In fact both the definability and truth lemma can fail for class forcing notions

For example one may try to define the following:

$p \Vdash \tau_1\in\tau_2 \leftrightarrow \{p':\exists (\tau_3,p'')\in \tau_2 \text{ such that } p'\leq p'', p'\Vdash \tau_2=\tau_3\}$ is dense below $p$.

But the logical complexity of such a statement depends on the ranks of the names and since the forcing is a proper class then the complexity of the statement cannot be bounded and thus determined.

Thus to determine whether a class forcing notion is definable, we will have to involve restrictions on the class forcing notions $\mathbb{P}$. One such property to impose on class forcing is the property of pretameness defined by Friedman:

A class forcing $\mathbb{P}$ is pretame if whenever we have an $(M,A)$-definable (where $A\subseteq M$) sequence of dense classes $\langle D_{\alpha}: \alpha\in X\rangle$ and $X\in M$, $p\in \mathbb{P}$, then there is a condition $q\leq p$ and a new sequence $\langle E_{\alpha}: \alpha\in X\rangle\in M$ with $E_{\alpha}\subseteq D_{\alpha}$ and $E_{\alpha}$ is predense below $q$ for every $\alpha\in X$.

In his book on Fine Structure and Class Forcing, Friedman shows that for any formula $\varphi$ the forcing relation is now $(M,A)$-definable. In addition the truth lemma also holds in this case. You will definitely find more information in that book.