# Generic reals in forcing iterations

Suppose that $(\mathbb{P}_{\alpha}, \underset{\sim}{\mathbb{Q_{\alpha}}} : \alpha<\beta)$ is a forcing iteration, and that for each $\alpha$, there is a name $\underset{\sim}{\eta_{\alpha}}$ for the generic real added at the $\alpha$th stage. Denote the limit of the iteration by $\mathbb{P}_{\beta}$. Does it follow that $\{\eta_{\alpha} : \alpha<\beta\}$ is generic for $\mathbb{P}_{\beta}$? Intuitively it seems true, but I don't know how to prove it.

-
In this generality the result is false $\{\eta_\alpha: \alpha<\beta\}$ is not even a filter (in general). I suppose you have in mind some forcing notions where the generic real code the generic filter like in Cohen, Sacks, Laver forcings... –  azarel Mar 28 '12 at 2:50
Yes, of course. You may assume that we're dealing with a nice situation where the generic filter is coded by the generic real. –  measurable cardinal Mar 28 '12 at 2:58
If I interpret $\{\eta_\alpha:\alpha<\beta\}$ literally, as just the set of these reals, then the answer is no. For example, if I do a finite-support iteration of Cohen forcing for $\omega$ steps, the set of Cohen reals that I adjoined doesn't determine the final model, but the sequence of them does.
So let me assume that you meant the sequence $\langle\eta_\alpha:\alpha<\beta\rangle$ instead. Under reasonable assumptions about how the generic filters are determined by the reals (as you intended, according to your comment of March 28), knowing the sequence $\langle\eta_\alpha:\alpha<\beta\rangle$ means knowing the sequence of generic filters for all the intermediate forcings $\mathbb P_\gamma$. That sequence should be enough to determine the generic filter for $\mathbb P_\beta$. The nontrivial case would be the case where $\beta$ is a limit (and this might be the only case you originally intended). Here the complete Boolean algebra associated to $\mathbb P_\beta$ must be generated (as a complete Boolean algebra, in the ground model) by the union of the complete Boolean algebras associated to the earlier $\mathbb P_\gamma$'s. The definition of genericity of ultrafilters immediately gives that, if you know the restriction of a generic ultrafilter to a set of generators of your algebra, then you know the whole ultrafilter.
Two clarifications: (1) "Set of generators" means with respect to infinitary Boolean operations in the ground model. (2) "Must be generated" means that, if the earlier Boolean algebras generate a proper complete subalgebra of the algebra associated to $\mathbb P_\beta$, then I don't think one should call $\mathbb P_\beta$ the result of an iteration. Note, though, that the details of how this generating occurs can depend on the type of iteration. For finite support iterations, it suffices to just take Boolean joins of elements coming from earlier stages. For other types of supports, it seems that one needs to take joins of meets.