Coloring trees in reverse mathematics

TL;DR

This paper investigates the reverse mathematical strength of the tree theorem for pairs ($ ext{TT}^2_2$), showing it is strictly between $ ext{RCA}_0$ and $ ext{ACA}_0$, and introduces new forcing techniques for tree-based combinatorial principles.

Contribution

It proves that $ ext{TT}^2_2$ does not imply $ ext{ACA}_0$, and provides a new proof that $ ext{TT}^2_2$ is stronger than $ ext{RT}^2_2$, establishing a new natural intermediate principle.

Findings

$ ext{TT}^2_2$ does not imply $ ext{ACA}_0$ over $ ext{RCA}_0$

$ ext{TT}^2_2$ is strictly stronger than $ ext{RT}^2_2$

Introduces an extension of bushy tree forcing for combinatorial statements on trees

Abstract

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