Effectiveness of hindman’s theorem for bounded sums

We consider the strength and effective content of restricted versions of Hindman’s Theorem in which the number of colors is specified and the length of the sums has a specified finite bound. Let HT^≤n_k denote the assertion that for each k-coloring c of ℕ there is an infinite set X ⊆ ℕ such that all sums Σ_x∈F x for F ⊆ X and 0 < |F| ≤ n have the same color. We prove that there is a computable 2-coloring c of ℕ such that there is no infinite computable set X such that all nonempty sums of at most 2 elements of X have the same color. It follows that HT^≤2₂is not provable in RCA0 and in fact we show that it implies SRT²₂in RCA₀ +BΠ⁰₁. We also show that there is a computable instance of HT^≤3₃with all solutions computing 0′. The proof of this result shows that HT^≤3₃ implies ACA₀ in RCA₀.