Coloring trees in reverse mathematics

The tree theorem for pairs ($\mathsf{TT}^2_2$), first introduced by Chubb, Hirst, and McNicholl, asserts that given a finite coloring of pairs of comparable nodes in the full binary tree $2^{<\omega}$, there is a set of nodes isomorphic to $2^{<\omega}$ which is homogeneous for the coloring. This is a generalization of the more familiar Ramsey's theorem for pairs ($\mathsf{RT}^2_2$), which has been studied extensively in computability theory and reverse mathematics. We answer a longstanding open question about the strength of $\mathsf{TT}^2_2$, by showing that this principle does not imply the arithmetic comprehension axiom ($\mathsf{ACA}_0$) over the base system, recursive comprehension axiom ($\mathsf{RCA}_0$), of second-order arithmetic. In addition, we give a new and self-contained proof of a recent result of Patey that $\mathsf{TT}^2_2$ is strictly stronger than $\mathsf{RT}^2_2$. Combined, these results establish $\mathsf{TT}^2_2$ as the first known example of a natural combinatorial principle to occupy the interval strictly between $\mathsf{ACA}_0$ and $\mathsf{RT}^2_2$. The proof of this fact uses an extension of the bushy tree forcing method, and develops new techniques for dealing with combinatorial statements formulated on trees, rather than on $\omega$.