PFA and the tree property at $\aleph_2$

Recall that a poset $\langle T,\le\rangle$ is said to be a $\lambda^+$-Aronszajn tree, if it isomorphic to a poset $(\mathcal T,\subseteq)$ of the form:

1. $\emptyset\in \mathcal T\subseteq{}^{<\lambda^+}\lambda$; Write $\mathcal T_\alpha:=\{\sigma\in\mathcal T\mid \text{dom}(\sigma)=\alpha\}$;
2. for all $\alpha<\lambda^+$, $\mathcal T_\alpha$ has size $\le\lambda$, say $\mathcal T_\alpha=\{ T_\alpha^i\mid i<\lambda\}$;
3. if $\sigma\in\mathcal T$ and $\alpha<\lambda^+$, then there exists $\tau\in\mathcal T_\alpha$ such that $\sigma\cup\tau\in{}^{<\lambda^+}\lambda$;
4. $\mathcal T$ has no cofinal branches, i.e., $\bigcup t$ is not in ${}^{\lambda^+}\lambda$ for every $t\in\prod_{\alpha<\lambda^+}\mathcal T_\alpha$.

Kurepa found a connection between the Souslin problem and the above sorts of trees. In particular, he introduced the notion of an $\aleph_1$-Souslin tree (in the above terminology – an $\aleph_1$-Aronszajn tree plus requirement #5 which I will not define here) and showed that such a tree provides a counterexample to the Souslin problem.
Failing to construct such a tree, Kurepa once asked his fellow, Aronszajn, whether an $\aleph_1$-tree satisfying (1)–(4) exists. Aronszajn proved it does! Kurepa, who did not seem to appreciate this “poor man’s Souslin tree”, labeled this tree – as a joke – by Aronszajn tree.

So, we know that an $\aleph_1$-Aronszajn tree exists. How about $\aleph_2$-Aronszajn trees? In this post, we shall see that PFA rules them out.

Theorem (Baumgartner). PFA implies the tree property holds at $\aleph_2$.
That is, if PFA holds, then there are no $\aleph_2$-Aronszajn trees.
Proof. Assume PFA. In particular, $2^{\aleph_0}=\aleph_2$.
Suppose towards a contradiction that $\mathcal (T,\subseteq)$ is an $\aleph_2$-Aronszajn tree as above. Let $\mathbb P$ denote Levy’s notion of forcing for collapsing $\omega_2$ to $\omega_1$.   Let $o_1$ and $o_2$ denote $\omega_1$ and $\omega_2$ of $V$, respectively. In $V^{\mathbb P}$, let $c:o_1\rightarrow o_2$ be an increasing cofinal map. Define $\mathcal T’:=\bigcup\{\mathcal T_{c(\alpha)}\mid \alpha<\omega_1\}$. As $\mathbb P$ is $\sigma$-closed, Silver’s lemma together with $\aleph_1<2^{\aleph_0}$ tells us that $\mathcal T’$ admits no cofinal branches. As $(\mathcal T’,\subseteq)$ is a tree with no uncountable chains, we may pick a c.c.c. notion of forcing $\mathbb Q$ that specializes it. This means that in $V^{\mathbb P*\mathbb Q}$, there exists $f:\mathcal T’\rightarrow\omega$ such that $f(\sigma)\neq f(\tau)$ for all $\sigma\subset \tau$ in $\mathcal T’$.
It follows that for every $\alpha,i<\omega_1$, the set $$D_{\alpha,i}:=\{ p\in\mathbb P*\mathbb Q\mid \exists(\beta,n)\in\omega_2\times\omega, p\Vdash c(\alpha)=\beta\ \&  f(T^i_\beta)=n\}$$ is dense-open. Since $\mathbb P*\mathbb Q$ is proper, and PFA holds, let us pick a pseudo-generic set $G$ that meets $D_{\alpha,i}$ for all $\alpha,i<\omega_1$.
Define $d:\omega_1\rightarrow\omega_2$ by letting $c(\alpha):=\beta$ iff there exists some $p\in G$ such that $p\Vdash c(\alpha)=\beta$. Clearly, $d$ is an increasing map, and $\delta:=\sup(d[\omega_1])$ has cofinality $\omega_1$.
By condition (3), let us pick some $t\in\mathcal T_\delta$. Note that by condition (3) again, we have $T:=\{t\restriction d(\alpha)\mid \alpha<\omega_1\}\subseteq\mathcal T$.
Define $g:T\rightarrow\omega$ by letting $g(\sigma):=n$ iff there exists some $p\in G$ such that $p\Vdash f(\sigma)=n$.
Finally, pick $\alpha_0<\alpha_1<\omega_1$ such that $g(t\restriction d(\alpha_0))=g(t\restriction d(\alpha_1))$. Then we get a contradiction to the fact that $t\restriction d(\alpha_0)\subset t\restriction d(\alpha_1)$. $\square$