Impact of discrepancy between Kunen's and Jech's definition of iterated forcing on full support iterations One of the first things we usually learn when we study iterated forcing is that we can force over a model of ZFC + GCH to make the continuum function ($\lambda \mapsto 2^{\lambda}$) restricted to some set $S$ of regular cardinals follow any nondecreasing pattern satisfying König's Theorem ($\text{cof}(2^{\lambda}) > \lambda$).  This is accomplished by an Easton product of adding the desired number of Cohen subsets to each cardinal in $S$.  For example, assuming that the GCH holds in $V$, we can force $2^{\aleph_n} = \aleph_{n+2}$ for all Natural numbers $n$ with the full support $\omega$-iteration where we force with the ground model poset adding $\aleph_{n+2}$ many Cohen subsets of $\aleph_n$ at every stage $n$.
However, if we instead force with the posets adding $\aleph_{n+2}$ Cohen subsets of $\aleph_n$ from the successive extensions, then the iteration will preserve the GCH.  Such a phenomenon is easily explained away by the fact that after forcing to add Cohen subsets of $\aleph_n$, we have necessarily changed the definition of the forcing adding Cohen subsets of $\aleph_{n+1}$ in the extension.

Now consider a full support $\omega$-iteration $\mathbb{P}$ where at every stage $n$, we force to add a Cohen real.  Since the poset adding a Cohen real is the set of finite partial binary sequences with domain $\omega$, all transitive models of ZFC agree on its definition.  Therefore, the aforementioned concern disappears in this context.  Because the forcing to add a Cohen real satisfies the countable chain condition (c.c.c.), it is proper.  Then since proper forcing is closed under countable support iterations using Jech's definition of a forcing iteration, $\mathbb{P}$ will be proper and hence $\omega_1$-preserving.  However, using Kunen's definition, the iteration can collapse $\omega_1$.  For example, from Chapter VIII, Exercise (E4): 
Let $\mathbb{P}_{\omega}$ be defined by countable supports, and let each $\pi_n$ be $(\text{Fn}(\omega, 2)){}^{\check{}}$).  Show that $\mathbb{P}_{\omega}$ collapses $\omega_1$.
Kunen then notes that this problem goes away when full names are used.  On the other hand, Jech seems to circumvent the problem altogether by defining $\mathbb{P}_n * \dot{\mathbb{Q}}_n$ to be the set of pairs $\langle p, \dot{q}\rangle \in \mathbb{P} \times \text{dom}(\dot{\mathbb{Q}}_n)$ such that all conditions from $\mathbb{P}_n$ force $\dot{q}$ to be in $\dot{\mathbb{Q}}_n$ rather than just requiring that the condition $p$ forces this as Kunen does.
What I would like to see then is an elaboration of the explanation of why these forcing iterations are different including the intuition behind these differences.  Specifically, my question is as follows:

Why does the full support $\omega$-iteration forcing with $(\text{Fn}(\omega, 2)){}^{\check{}}$ (forcing to add a Cohen real) at every stage collapse $\omega_1$ under Kunen's definition but not under Jech's?  For example, how is it that every binary $\omega$-sequence from the ground model is coded in the generic filter using Kunen's definition but not Jech's?

As a side request related to how this question came up, can you provide an example of a full support $\omega$-iteration that must have size at least $\aleph_2$, but each individual stage of forcing is necessarily proper and of size at most $\aleph_1$?
 A: I hope I can answer this question in a reasonable way.  The natural way to define the iteration $\mathbb P*\dot{\mathbb Q}$ is to consider all pairs $(p,\dot q)$ with 
$p\in\mathbb P$ and $p\Vdash\dot q\in\dot{\mathbb Q}$.
Unfortunately this is a proper class.  (The definition in Jech's book also gives a proper class.)
The problem in Kunen's definition of the iteration $\mathbb P*\dot{\mathbb Q}$ is not so much that he defines 
$(p,\dot q)\in\mathbb P*\dot{\mathbb Q}$ if $p$ forces $\dot q$ to be in $\dot{\mathbb Q}$,
but that he only considers names $\dot q$ in the domain of $\dot{\mathbb Q}$.
He does this to make sure that the iteration $\mathbb P*\dot{\mathbb Q}$ is a set rather than a proper class.
But there are other ways to make sure that the iteration is a set, for example by allowing 
arbitrary names for $\dot q$ that are in some sufficiently large $H_\chi$ (sets with transitive closure of size $<\chi$).
"Sufficiently large" depends on $\mathbb P$ and $\dot{\mathbb Q}$. 
Now Jech only considers pairs $(p,\dot q)$ such that $\dot q$ is forced by $1_{\mathbb P}$ to be in $\dot{\mathbb Q}$.   But this doesn't really make a difference since by the existential completeness lemma, if $p\Vdash\dot q\in\dot{\mathbb Q}$, then there is a name $\dot r$ which is forced by $1_{\mathbb P}$ to be a condition in $\dot{\mathbb Q}$ and such that $p\Vdash\dot q=\dot r$.  
Now in the case of a two step iteration, the definitions by Jech and Kunen are equivalent,
and both are equivalent to the one that I suggested (arbitrary names in the second coordinate, but cutting off somewhere).
The right way to see this is to first show that if you cut off Jech's iteration at a sufficiently large $H_\chi$, then you get a dense subset of Jech's iteration.
This cut off version of Jech's iteration is dense in my version (with the same sufficiently large $H_\chi$). 
Now Kunen's iteration is equivalent to mine since given $(p,\dot q)$ in my iteration,
there are $s\leq p$ and $\dot t$ in the domain of $\dot Q$ such that 
$s\Vdash\dot q=\dot t$.  We have $(s,\dot t)\leq(p,\dot q)$, showing that Kunen's iteration is dense in mine.  
Things start to fall apart if we go to longer iterations, and iterations with infinite support.  My argument above still shows that Kunen's iteration of arbitrary length, with finite supports, is equivalent to my version for long iterations.
This is because given a finitely supported condition in the long iteration in my sense,
say with support of length $n$, you can decrease the first $n-1$ coordinates to force the last coordinate to be something given by a name in the domain of the respective name of a partial order.  Then you decrease the first $n-2$ coordinates to take care of the $n-1$-th coordinate and so on.   
This argument clearly does not go through with countable supports.  Hence the countable support iteration in Kunen's sense is not necessarily equivalent to my version or Jech's version.  It is equivalent, however, if all the iterands are given by full names.
Now, what is the problem in terms of properness?  The proof of properness of countable support iterations of proper forcing (and I am referring to the proof in Goldstern's 
"Tools for your forcing construction") makes frequent use of the existential completeness lemma to cook up names for conditions.  Now in the Kunen version of the iteration
it may happen that these names cannot be used since they may not be in the domain of the respective name for a partial order.  
And in fact, as the exercise shows, even the countable support iteration of Cohen forcing
of length $\omega$ in Kunen's sense depends on which names you choose for the iterands:
Full names yield a proper forcing (which would be equivalent to the iteration in my sense),
but taking canonical names yields a forcing notion that collapses $\omega_1$.
I hope this helps.
