Minimal model over forcing iteration Suppose we define over $M$ some sequence of iterated forcing $\mathbb{P}_\alpha$ for $\alpha<\delta$: $M_\alpha = M[G_\alpha]$ where $G_\alpha$ is generic in $\mathbb{P}_\alpha$. Now in the limit stage we pick some support (full, finite, countable or something more wacky), and get model $M_\delta = M[G_\delta]$.
Question is - could there be some model $N$ of $\mathsf{ZF}$ such that $M_\delta\supsetneq N\supseteq\bigcup\limits_{\alpha<\delta}M_\alpha$?
 A: Sometimes, but not always.
Consider Feferman's model, which is the first example of a model in which $\omega$ does not carry any free ultrafilter. This model can be presented as taking a finite support iteration of length $\omega$ where we add Cohen reals, and then consider an intermediate model which contains all the reals, but not the set of reals. You can find this formalized in this way in my paper,

Asaf Karagila, Iterating Symmetric Extensions. ArXiv 1606.06718, under review

Similarly, Feferman's model where $\sf DC$ holds is obtained by adding $\omega_1$ (or any uncountable number of) Cohen reals, and considering $L(\Bbb R)$ (rather $V(\Bbb R)$, but he starts with $L$), and this can also be considered an intermediate model to a countable support iteration of adding Cohen reals which lies between the full extension and contains all the intermediate models.
But on the other hand, considering self-coding generics. Assume $V=L$, and add a Cohen real $c_0$; then take the product over $n\in c_0$ of adding a Cohen generic to $\omega_n$, this is now $c_1$ which is a generic subset of $\omega_\omega$; then take the product of $\alpha\in c_1$, adding a Cohen subset to $\omega_\alpha$. Rinse, wash, repeat. At the first limit step, you get a new subset of the first fixed point, and this new subset codes itself. Namely, if you take all the finite steps of the iteration, then the full extension is also there, as it is determined completely by which cardinals below the first fixed point have a Cohen subset.
The reason is that the first two examples have sufficient homogeneity, whereas the third one is an example of a pointwise homogeneous iteration which is rigid (there are no automorphisms of the iteration). I don't think there is a good characterization as to when there are such intermediate models, but homogeneity of the iteration plays a role.
