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$?