The Meta-Mathematics of Multiple Forcing In forcing we have the forcing theorem (also called the truth and definability theorem). It guarantees that forcing works. What are the similar theorems for multiple forcing?
To elaborate: Kunen, in his Set theory book uses forcing repeatedly to build a finite chain of models $M_\alpha$ such that the final model satisfies the continuum being $\aleph_{2}$ and $2^{\aleph_{1}}=\aleph_{2}$ but not GCH. The fact that each of these models behave as they should follows from the forcing theorem. However if you try to do this for infinite $\alpha$, you'll have a "proof of infinite length" which doesn't make sense. 
I know that it is possible to substitute a single forcing that achieves the multiple forcing and hence the original forcing theorem will apply and we can argue about the generic model using the ground model as usual. But it is not clear, how the forcing theorem will look like for the intermediate models. Is there even one? Or is the existence of intermediate models there to guide our intuition? 
Edit1: After Asaf's answer I wanted to emphasize a certain part of my question. I'm fine with the idea of finding a poset that does what the iterated forcing does, as it relates to the forcing theorem. However, iterated forcing is presented in such a way that makes it seem like you have models $M_\alpha$ laying around. I'm a little confused about if or how we access them. If we are doing for instance a iteration of length $\omega_{2}$, can we talk explicitly about how the model indexed by $\omega_{1}$ looks like? and how truth there depends on the model that came before it? or is this somehow built in to the recursion? If it is, it is unclear to me.  
For example is there something like: for any formula $\varphi$, there is a formula $\psi$ such that $ZFC\vdash$ for any ordinals $\alpha,\beta, \alpha<\beta$ $M_{\beta}\models\varphi$ iff there is some $p\in{G_{\alpha}}$, a forcing poset in $M_\alpha$ s.t. $M_{\alpha+1}\models{\psi}$? I'm not seeing exactly how the recursion works. 
 A: What you call "multiple forcing" is called "iterated forcing". And the entire amazing thing is that you can find a single forcing poset in the ground model, which accomplishes this iteration in one go. So what we do, usually, is define by recursion this partial order.
We often find it easier to "access the models", because names of iterated forcing can be slightly more irritating to handle than usual. But the point is that if we can find some partial order with the wanted properties, then some conditions in the generic forced that; so below that condition we know what name we want. If we cannot prove that there is always such condition forcing the existence of a partial order to our liking, then we can always give up and say "below a condition forcing no such order, take the trivial forcing".
But the meta-mathematics of iterated forcing is indeed nontrivial. If we just take one forcing extension at a time, there is absolutely no guarantee that we can find a model which combines the chain of models we have constructed. We can just iterate Cohen forcings, one after another, and at the $\omega$ step, we have a sequence of reals such that the first coordinate in each real encodes a collapse of the entire universe to be countable.
So in any case, choosing generic filters one at a time may not work, if you want to iterate this to a transfinite length. What the generic filter for the iterated forcing gives you is a filter whose coordinates are pointwise generic over the models constructed thus far, but with additional conditions to ensure that these models coalesce into a single model of $\sf ZFC$ at the end.
