Suppose that $\langle\mathbb{P\_\alpha,\dot Q\_\beta}\mid \beta<\delta,\alpha\leq\delta\rangle$ is a system of iterated forcing.


Let $\dot a$ be a name in $\mathbb P\_\delta$, and let $G\_\alpha$ be a generic for $\mathbb P\_\alpha$ for $\alpha<\delta$. Is there a reasonable sense in which we can interpret $\dot a$ using $G\_\alpha$?


If so, is the result of this partial interpretation a $\mathbb P\_{\alpha\delta}$-name (i.e. the quotient forcing) for $\dot a$?


(If it matters, we can assume that the iteration is finite support, but a general answer would be great.)



Partial interpretation of an iteration
$\newcommand\P{\mathbb{P}}\newcommand\Q{\mathbb{Q}}$


Yes. Perhaps it is easier to think about the case of two-step iterations, which contain the whole story. Namely, from any $\P\*\dot\Q$-name $\dot a$ we may in a canonical manner construct a $\P$-name for a $\dot\Q$-name, let us call it $\ddot a$, such that if $V\subset V[G][H]$ is the forcing extension first by $G\subset\P$ and then by $H\subset\Q=\dot\Q\_G$, then $\dot a\_{G\*H}=(\ddot a\_G)\_H$. That is, $\ddot a$ is a name for an object in $V[G]$ that will be a $\Q$-name for the object in $V[G\*H]$ named by $\dot a$. One may view it as an exercise in parenthesis-rearranging to construct $\ddot a$ from $\dot a$, if you think about what needs to be in $\ddot a$, given what is in $\dot a$. So you can make a recursive definition working directly with the names. 


But also, you can see abstractly that this must be true, simply because $V[G\*H]=V[G][H]$, so every object in $V[G\*H]$ is the result of interpreting a $\Q$-name in $V[G]$ by the filter $H$. In particular, $\dot a\_{G\*H}$ must be $\tau\_H$ for some $\Q$-name $\tau$ in $V[G]$, and $\tau$ itself must be $\ddot a\_G$ for some $\P$-name (of a $\dot\Q$-name) $\ddot a$. 


Your case of iteration is just like this simple two-step iteration, if you think of the iteration up to stage $\alpha$ as one step, and then the rest of the iteration from $\alpha$ to $\delta$ as the second step. 


