Preservation Results for Iterations of Non-Proper Forcing Suppose $\mathbb{P}$ is a forcing with the following properties: Let $G \subseteq \mathbb{P}$ be filter generic over $V$, then there exists $A \in V[G]$ such that $V[G]$ thinks $A$ is countable and $A \subseteq {}^\omega 2 \cap V$, but $A$ is not covered by any ground model countable set. That is, in the generic extension there is a countable set of ground model reals that can not be covered by a countable set from the ground model.
Certainly $\mathbb{P}$ is not a proper forcing. 
Is it possible that $\mathbb{P}$ can preserve $\aleph_1$? As $A$ need not be a set in $V$, it seems at least theoretically possible that $\mathbb{P}$ does not need to collapse any cardinals. 
Now I would like to iterate this forcing by itself. However, since it is not proper, I do not know what properties can be expected to be preserved. 
Although this may be a bit too open ended, my next question is : What classes of forcing (by which I means things like c.c.c., proper, semi-proper, etc) could $\mathbb{P}$ potentially belong to given that it adds a countable set of ground model real that can not be covered by a countable ground model set. (Certainly $\mathbb{P}$ can not be c.c.c. or proper.)
Do any of these classes have preservation theorems for iterations (countable support or perhaps some other type of iterations)? I am most interested in perserving $\aleph_1$, preserving ${}^\omega\omega$-bounding, or $\aleph_2$-chain conditions. If it is applicable, one may assume $\mathbb{P}$ has size $\aleph_1$ if $\mathsf{CH}$ holds. 
I am looking for some class of forcing that can help handle iterations of non-proper forcings like $\mathbb{P}$. Thanks for any information that can be provided. 
 A: Chapters X, XI and XV (possibly also others) in Shelah's book "Proper and Improper Forcing" deal with the problem of iterating nonproper forcing notions. (By this I mean very non-proper. E.g., not even $S$-proper for any stationary $S$.) 


*

*Chapter X gives a definition of revised countable support iteration (RCS). (It is somewhat difficult to read, but there are other definitions in the literature which could be used instead. 

*Chapter XI deals with nonproper iterations not adding reals over models of CH. There is a property of forcing notions $Q$ that I will call $Pr_{X}(Q)$ that satisfies:  Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$ and moreover does not add reals.  AND:  The limit of an RCS iteration (that uses lots of collapses) of forcing notions with $Pr_X$ will itself have property $Pr_X$. 

*Chapter XV introduces a property that I will call $Pr_{XV}$ and proves a similar statement: Any forcing which has property $Pr_X(Q)$ preserves $\omega_1$  AND:  The limit of an RCS iteration (that uses lots of collapses) of forcing notions with $Pr_{XV}$ will itself have property $Pr_{XV}$. 


A main point is that Namba forcing $Nm$ satisfies both of these properties. (Regardless of whether $Nm$ is semiproper or not. There are several versions of $Nm$: Laver-like or Miller-like, using the club filter or the cobounded filter;  I am not sure if all of them have these properties.) 
Roughly speaking,  $Pr_{XV}(Q)$ is this: whenever you have a sufficiently nice tree $(N_\eta: \eta\in \omega_2^{<\omega})$ of countable elementary submodels of the universe, where niceness in particular implies that the intersections of the models with $\omega_1$ converge to the same ordinal $\delta$ along every branch, then $Q$ forces that there exists a branch $\nu\in \omega_2^\omega$ such that $N_\nu[G]\cap \omega_1=N_\nu\cap \omega_1=\delta$. As I recall, if $Q=Nm$ then the generic branch $\nu$ (the union of all stems of conditions in the generic filter) will satisfy the requirement. 
A: The existence of a forcing notion $\mathbb{P}$ like that is equivalent to $\neg\text{CH}$. 
On the one hand, Noah's comment shows that if CH holds, then one cannot add a countable set of ground-model reals that is not covered by any countable ground model set, while preserving $\omega_1$.
Conversely, suppose that CH fails in $V$, and consider Namba forcing. This adds a new cofinal $\omega$-sequence in $\omega_2^V$, and hence because $\neg\text{CH}$ it adds a countable set of ground-model reals, which is not covered by any ground-model countable set, or indeed by any ground model set of size $\omega_1$ in the ground model, but it preserves $\omega_1$. QED
It seems to be consistent relative to large cardinals that Namba forcing is semi-proper, in which case one might hope to iterate it.
Here is another kind of example. Start in $V$ with a measurable cardinal $\kappa$, and let $V[G]$ be the extension obtained by adding $\kappa$ many Cohen reals, so that $2^\omega=\kappa$ in $V[G]$. Now, in $V[G]$, let $\mathbb{P}$ be Prikry forcing for a normal measure $\mu$ in $V$, as defined in $V$. If $H\subset\mathbb{P}$ is $V[G]$-generic, then we can view $V[G][H]$ as $V[H][G]$, that is, as first doing Prikry forcing, and then adding reals. So all cardinals are preserved. But the Priky sequence will add a new $\omega$-sequence cofinal in $\kappa$, and hence a new countable set of reals from $V[G]$, which is not covered by any set in $V[G]$ of size less than $\kappa$ in $V[G]$. Thus, forcing over $V[G]$ with the Prikry forcing of $V$ has your desired properties. 
And there are various complicated ways to iterate Priky forcing, depending on what you want to accomplish, and what kind of large cardinals you have available. 
