Why do we define an inner forcing relation?

Question

Studying forcing I came across different definitions of the forcing relation $\Vdash$:

• the outer forcing relation $\Vdash^M$ where we define $p \Vdash^M \varphi(\tau_0,\dotsc,\tau_n)$ to hold if for every generic $G$ with $p \in G$ we have $\varphi^{M[G]}(\tau_0^G,\dotsc,\tau_n^G)$.
• the inner forcing relation $\Vdash^*$ defined recursively using dense sets.

I understand that the latter allows to speak about generic extensions within the ground model $M$ without having to deal with generic filters etc. This seems to be important because working in $M$ we don't know if there even exists a generic extension.

However, I don't see the advantage of using the inner forcing relation. In our lecture, for proving statements we almost always used the inner forcing relation which seemed to make the proofs more complicated. In particular, we have proven the forcing theorems and know that both definitions are "equivalent" in some sense.

So my question is, why is the inner forcing relation necessary? Why do we work with it? Is it just to avoid working in countable models before doing the actual consistency proofs?

Answer 1

The recursive definition is the common way of proving that the forcing relation is definable in the ground model, which is not at all clear from the generic filter definition.

When one wants to analyze both the ground model and some generic extension, the definability of the forcing relation is used. For instance, if you wanted to prove that $\aleph_1$-closed forcings do not add any new reals, you may go about it as follow: Let $\tau$ be a $\mathbb{P}$-name such that there some $p \in G$ with $p \Vdash \tau$ is a real. Let $q \leq p$ be arbitrary. Let $q_0 < q$ and $a_0 \in \{0,1\}$ such that $q_0 \Vdash \tau(\check 0) = a_0$. Suppose $q_n$ has been defined, let $q_{n + 1} \leq q_n$ and $a_{n + 1} \in \{0,1\}$ be such that $q_{n + 1} \Vdash \tau(\check{n + 1}) = a_{n + 1}$. By $\aleph_1$-closed, let $t\leq q_n$ for all $n$. Then using the definability of the the forcing in $M$, you apply the separation axiom in $M$, to conclude there is a real $r \in M$ such that for all $n$, $r(n) = a_n$. By a genericity argument, $M[G] \models \tau = \check r$.

So the definability of the forcing relation was essential to the above. However, I did not ever explicitly use the recursive definition of the forcing relation. This is generally how forcing arguments go. I am not exactly sure what you mean by "for proving statements we almost always used the inner forcing relation".

Certainly, if you prove abstract theorems about forcing and names, you may find that knowing explicitly how the forcing relation evaluates may be useful. For example, if you are trying to the prove fullness or the maximality principle.

Answer 2

The inner definition is particularly useful when you have to use reflection arguments.

For example, you want to show that if you start with a large cardinal (e.g. a weakly compact) and you do some kind of forcing, then you have the large cardinal as the new $\omega_1$ or $\omega_2$, and some sort of combinatorial principle fails (e.g. $\omega_2$ has the tree property).

The way we usually go about this is to say "If there was a counter example to the wanted property, then we can find an initial segment of the forcing where this was also true, but bla bla bla". The way we obtain this initial segment is by using the definability of the forcing relation (and the large cardinal properties which allow us some limited reflection of these sort of statements).

Similarly when you want to talk about class forcing, it is sometimes useful since you can find some large enough $\alpha$, such that $V_\alpha$ reflects both the forcing and the inner forcing relation for a particular formula. This can be very useful when you want to prove that a class forcing preserves $\sf ZFC$, something which can be easily broken with a class forcing.

Answer 3

Try avoiding internal forcing while showing the following: In every Cohen real extension, every $\omega$-sequence of ordinals equals a ground model $\omega$-sequence infintely often.

Let me know if this seems boring and I will give you harder ZFC facts.

Answer 4

Reference:"Set Theory : An Introduction to Independence Proofs" by Kunen (chapter 7). It's the Decidability Lemma. For a formula F , and a poset P in the ground model M the set of x in P which force F (over P) is a MEMBER of M. This is a useful and crucial tool in many results.