Countable support iteration of proper forcings and the tree property

Question

I'm mainly concerned with countable support iterations of proper forcings that add reals of some large cardinal length. It is known that countable support iteration of Sacks forcing/Cohen forcing of weakly compact ($\kappa$) length forces $\kappa=\omega_2$ has the tree property. Is there a general theorem, like: for any $\langle P_i, \dot{Q}_j: i\leq \kappa, j<\kappa\rangle$ countable support iteration of proper forcings that add reals for some large cardinal $\kappa$ (weakly compact), then the tree property at $\omega_2$ holds in the forcing extension? Note $2^\omega=\kappa=\omega_2$ in the extension.

Edit: for larger cardinals as Sean Cox pointed out, the answer is positive.

Answer 1

If $\kappa$ is huge, then any countable support iteration $\mathbb{P}$ of proper forcing up to $\kappa$ (where each component is of size $<\kappa$) that forces $2^\omega = \kappa = \omega_2$, must also force the tree property at $\omega_2$.

To see this, suppose $j: V \to N$ is a huge embedding with critical point $\kappa$. The assumptions on $\mathbb{P}$ ensure that if $G$ is $(V,\mathbb{P})$-generic, the quotient $j(\mathbb{P})/G$ is proper from the point of view of $N[G]$, and by closure of $N$ in $V$, this quotient is proper from the point of view of $V[G]$ as well (because $V[G]$ sees that it really is a CS iteration of proper forcings). Then $V[G]$ sees that the poset $j(\mathbb{P})/G$ is a proper forcing that introduces a generic elementary embedding with critical point $\omega_2$. By the proof of Theorem 5 in my Chang's Conjecture and semiproperness of nonreasonable posets, this implies that $V[G]$ satisfies a strong form of Chang's Conjecture that I call $\text{SCC}^{\text{cof}}_{\text{gap}}$ (this is just a minor variation of an argument of Hiroshi Sakai). By a result of Torres-Perez and Wu (``Strong Chang’s Conjecture and the tree property at $\omega_2$"), together with failure of CH this implies the tree property at $\omega_2$.

(Edit: I see now that, due to a newer theorem of Torres-Perez and Wu in "Strong Chang's Conjecture, Semi-Stationary Reflection, the Strong Tree Property and two-cardinal square principles", in $V[G]$ you actually get the Strong Tree Property at $(\omega_2,\lambda)$ for all $\lambda < j(\kappa)$, since the kind of parameterized Strong Chang's Conjecture they use in that paper holds in $V[G]$ below $j(\kappa)$. In particular, $V_{j(\kappa)}[G]$ models the full Strong Tree Property. Also, as Jing pointed out in the comments below, you don't really need hugeness for this; strong compactness of $\kappa$ is enough. NOTE: the abstract in the Torres-Perez and Wu paper fails to mention failure of CH, which is of course required for their proof in Section 3).

Even if $\mathbb{P}$ is an RCS iteration of semiproper posets (each of size $<\kappa$), you get the same result. The only difference is that the generic elementary embedding is obtained by a semiproper (rather than proper) forcing, but that's still enough (by Sakai's argument) to get what I call $\text{SCC}^{\text{cof}}$ and apply the Torres-Perez and Wu theorem.

Also note that in many cases, measurability of $\kappa$ is enough to run the argument. You just need that the individual posets used in the $j(\mathbb{P})/G$ iteration are not only proper in the generic extension of $N$, but also in the corresponding generic extension of $V$. There should be plenty of scenarios where $\kappa$-closure of $N$ in $V$ (rather than $j(\kappa)$-closure) is enough to obtain that (and similarly for the RCS iteration of semiproper).