PFA and the tree property at ${\mathrm{\aleph }}_2$

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

1. $\mathrm{\varnothing }\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 ${\mathrm{\aleph }}_1$-Souslin tree (in the above terminology – an ${\mathrm{\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 ${\mathrm{\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 ${\mathrm{\aleph }}_1$-Aronszajn tree exists. How about ${\mathrm{\aleph }}_2$-Aronszajn trees? In this post, we shall see that PFA rules them out.

Theorem (Baumgartner). PFA implies the tree property holds at ${\mathrm{\aleph }}_2$.
That is, if PFA holds, then there are no ${\mathrm{\aleph }}_2$-Aronszajn trees.
Proof. Assume PFA. In particular, $2^{{\mathrm{\aleph }}_0}={\mathrm{\aleph }}_2$.
Suppose towards a contradiction that $\mathcal{(}T,\subseteq )$ is an ${\mathrm{\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\to o_2$ be an increasing cofinal map. Define ${\mathcal{T}}^{\prime }:=\bigcup \{{\mathcal{T}}_{c(\alpha )}\mid \alpha <{\omega }_1\}$. As $\mathbb{P}$ is $\sigma$-closed, Silver’s lemma together with ${\mathrm{\aleph }}_1<2^{{\mathrm{\aleph }}_0}$ tells us that ${\mathcal{T}}^{\prime }$ admits no cofinal branches. As $({\mathcal{T}}^{\prime },\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}\ast \mathbb{Q}}$, there exists $f:{\mathcal{T}}^{\prime }\to \omega$ such that $f(\sigma )\ne f(\tau )$ for all $\sigma \subset \tau$ in ${\mathcal{T}}^{\prime }$.
It follows that for every $\alpha ,i<{\omega }_1$, the set $$D_{\alpha ,i}:=\{p\in \mathbb{P}\ast \mathbb{Q}\mid \mathrm{\exists }(\beta ,n)\in {\omega }_2\times \omega ,p⊩c(\alpha )=\beta \mathrm{\&}f(T_{\beta }^i)=n\}$$ is dense-open. Since $\mathbb{P}\ast \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\to {\omega }_2$ by letting $c(\alpha ):=\beta$ iff there exists some $p\in G$ such that $p⊩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\upharpoonright d(\alpha )\mid \alpha <{\omega }_1\}\subseteq \mathcal{T}$.
Define $g:T\to \omega$ by letting $g(\sigma ):=n$ iff there exists some $p\in G$ such that $p⊩f(\sigma )=n$.
Finally, pick ${\alpha }_0<{\alpha }_1<{\omega }_1$ such that $g(t\upharpoonright d({\alpha }_0))=g(t\upharpoonright d({\alpha }_1))$. Then we get a contradiction to the fact that $t\upharpoonright d({\alpha }_0)\subset t\upharpoonright d({\alpha }_1)$. $\mathrm{<img\; draggable="false"\; role="img"\; class="emoji"\; alt="◻"\; src="https://s.w.org/images/core/emoji/15.0.3/svg/25fb.svg">}$