# Cardinality of Countable Support Iteration of Proper Forcing

Suppose $\mathsf{CH}$ holds. Suppose $\mathbb{P}$ is a forcing such that $\mathsf{ZFC} \models \mathbb{P} \text{ is proper and } |\mathbb{P}| = 2^{\aleph_0}$. For instance, Sacks forcing is such an example. Also it is important to note that although $\mathsf{CH}$ holds, $\mathsf{ZFC}$ proves that the cardinality of $\mathbb{P}$ is always the continuum.

Now let $\mathbb{P}_{\omega_1}$ denote the $\omega_1$-length countable support iteration of $\mathbb{P}$, that is iterating successively at each stage the name of the version of $\mathbb{P}$ from the previous stage. The question is: what is essentially the cardinality of $\mathbb{P}_{\omega_1}$? Is the cardinality of the iteration $\aleph_1$ in the sense that there is another forcing of size $\aleph_1$ which is forcing equivalent to $\mathbb{P}_{\omega_1}$?

In the definition of iterated forcing, elements of the iteration are defined using names. This could turn out to be a proper class. One of the tricks to deal with this is to take the name of minimal rank in classes of names forced to be equal. After using this trick, it is no longer clear to me exactly how large is the iteration. Even if it is larger than $\aleph_1$, could it still be forcing equivalent to a forcing of size $\aleph_1$?

You may assume that all elements of $P$ are hereditarily countable. Now let $P'_\alpha$ be the set of all hereditarily countable conditions in $P_\alpha$. Prove by induction that $P'_\alpha$ is dense in $P_\alpha$, for all $\alpha\le \omega_1$.
This is trivial if you use finite support iteration of ccc forcing. But it is still true for proper CS iterations, because even though there are names which are not hereditarily countable, you can translate them to "nice names", using antichains. Now these antichains may be uncountable, but (modulo an $N$-generic condition) you only care about their intersection with $N$.