The reverse mathematics of Hindman's theorem for sums of exactly two elements

Hindman's Theorem (HT) states that for every coloring of $\mathbb N$ with finitely many colors, there is an infinite set $H \subseteq \mathbb N$ such that all nonempty sums of distinct elements of $H$ have the same color. The investigation of restricted versions of HT from the computability-theoretic and reverse-mathematical perspectives has been a productive line of research recently. In particular, HT$^{\leqslant n}_k$ is the restriction of HT to sums of at most $n$ many elements, with at most $k$ colors allowed, and HT$^{=n}_k$ is the restriction of HT to sums of \emph{exactly} $n$ many elements and $k$ colors. Even HT$^{\leqslant 2}_2$ appears to be a strong principle, and may even imply HT itself over RCA$_0$. In contrast, HT$^{=2}_2$ is known to be strictly weaker than HT over RCA$_0$, since HT$^{=2}_2$ follows immediately from Ramsey's Theorem for $2$-colorings of pairs. In fact, it was open for several years whether HT$^{=2}_2$ is computably true. We show that HT$^{=2}_2$ and similar results with addition replaced by subtraction and other operations are not provable in RCA$_0$, or even WKL$_0$. In fact, we show that there is a computable instance of HT$^{=2}_2$ such that all solutions can compute a function that is diagonally noncomputable relative to $\emptyset'$. It follows that there is a computable instance of HT$^{=2}_2$ with no $\Sigma^0_2$ solution, which is the best possible result with respect to the arithmetical hierarchy. Furthermore, a careful analysis of the proof of the result above about solutions DNC relative to $\emptyset'$ shows that HT$^{=2}_2$ implies RRT$^{=2}_2$, the Rainbow Ramsey Theorem for $2$-colorings of pairs, over RCA$_0$. The most interesting aspect of our construction of computable colorings as above is the use of an effective version of the Lov\'asz Local Lemma due to Rumyantsev and Shen.