Countable support iteration of proper forcings and the tree property

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.

• I'd argue that for things like weakly-compact cardinals, the natural embeddings associated with them are enough to witness the tree property in the extension. The idea being that some fragment of $\Pi_1^1$ reflection remains in the extension. Which since you collapsed everything between it and $\omega_1$ would imply there would be a witness below $\omega_2$. – Not Mike Feb 15 '18 at 15:32
• But you want the tail to not add any cofinal branches – Jing Zhang Feb 15 '18 at 15:35
• Sacks and countably closed forcings don't add Branches to $\omega_1$-trees. – Not Mike Feb 15 '18 at 15:39
• Sure. The case for Sacks is known, countably closed forcing a don't add reals. My question is about the general proper forcing s that add reals – Jing Zhang Feb 15 '18 at 15:40
• It might have something to do with separating models. When you add a real, every countably closed ground model forcing is no longer countably closed in the extension (however it's still $\omega_1$-baire.) The idea here would be that the new real forced a set of new paths for countably closed partial orders, which they are happy to go down (stationarily often anyway.) – Not Mike Feb 15 '18 at 16:00

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).

• With respect to properness, wouldn't it simply be enough to witness winning strategies for the properness-game? Given the size assumptions on the iteration $\mathbb{P}$ that seems to only require countable closure. What am I missing? – Not Mike Feb 15 '18 at 21:24
• Yeah, for the strong tree property, the length you need is strongly compact (on the other hand, by Viale-Weiss it is necessary) since such iteration will always force the Semi-stationary reflection (which is equivalent to the strong Chang's Conjecture used in Torres-Perez and Wu's paper). So I think the question is only interesting in the case $\kappa$ is properly weakly compact. (there exists a $\kappa$-Aronszajn tree in the ground, the iteration can't add a path as it is $\kappa$-Knaster). – Jing Zhang Feb 15 '18 at 22:19
• @JingZhang Could you clarify what you meant in your last sentence? I don't understand your comment about "properly weakly compact". – Sean Cox Feb 15 '18 at 22:27
• @NotMike: I'm confused. Are you saying $V\models M^\omega\subset M$ then any proper forcing in $M$ is proper in $V$? I must have misunderstood you as that's not the case. Say $T$ is a distributive $\omega_1$ tree with no branch in $V$, the specializing forcing $S(T)$ is c.c.c, so proper in $V$. Now force with $T$, by distributivity $V^T\models V^\omega\subset V$ but then $S(T)$ is not proper in $V^T$ as forcing with it collapses $\omega_1$. – Jing Zhang Feb 16 '18 at 1:39
• @NotMike: that's not how you negate. there is $p\in j(P)$, for all strategy $\pi$, there exists names $\dot{\alpha}_i$, such that $p\Vdash \exists n \forall m \dot{\alpha}_n\neq \beta_m$, $\beta_i's$ are played according to the strategy. The witnesses $\dot{\alpha}_n$ change for each strategy. – Jing Zhang Feb 16 '18 at 3:15