Quotient Forcing in Iterations

177 Views Asked by At

I am trying to understand a proof of a lemma used to prove a preservation theorem for $^\omega \omega$-bounding for countable support iterations. In that quotient forcing is used to get a certain sequence of elements in the forcing iteration. To be more specific we are in the following situation: We consider countable support iteration of length $\omega$, and have a $P_\omega$-name $f$ for an element of $^\omega \omega$, we also have given some condition $p \in P_\omega$.

I will now just cite the passage I don't understand:

"Define $(q_n | n \in \omega)$ and $(\sigma_n | n \in \omega )$ such that $\sigma_0 \in \omega$ and $q_0 \leq p$ and $q_0 \Vdash_{P_\omega} ``f(0)= \sigma_0"$ and for every $n > 0$ we have that $\sigma_n$ is a $P_n$-name for an integer and $p \upharpoonright n \Vdash_{P_n} ``(q_n \in P_\omega \mathord/ G_{P_n}$ and $q_n \leq q_{n-1} \upharpoonright [n,\omega)$ and $q_n \Vdash `\sigma_n = f(n)`)"$.

There are no further details for this construction given. First, the definition of quotient forcing I am familiar with says that $P_\omega : P_n$ in $V[G_n]$ is $\{ p \in P_\omega |p \upharpoonright n \in G_n \}$ but i guess that translates to the definition used above where the end-segments of sequences are in the quotient forcing. Now, I do not understand how the sequence $(q_n|n \in \omega)$ can be constructed and in particular why we have that $p$ has so much information about the sequence without that we have to go below it. I guess that works in some way by getting a "dense property" below $p$ or $p \upharpoonright n$ and then choosing a antichain, and constructing the names $\sigma_n$ as antichain-names with respect to this antichain. But I am not sure whether the antichain should be chosen in $P_n$ or in $P_\omega$, and why we get one specific condition $q_n$ which knows that $\sigma_n$ is interpreted as $f(n)$ in every extension of $V[G_n]$ containing it.

I am sorry that I was not able to describe my problem more cleary, and hope that you can help me.