关于恰好两个元素之和的 Hindman 定理的逆数学

Hindman 定理（HT）指出，对于 $\mathbb N$ 的每种有限色着色，存在无限集 $H \subseteq \mathbb N$，使得 $H$ 中不同元素的所有非空和具有相同颜色。从可计算性理论和逆数学角度研究 HT 的限制版本近来已成为一条富有成果的研究路线。特别地，HT$^{\leqslant n}_k$ 是 HT 限制为至多 $n$ 个元素之和、至多允许 $k$ 种颜色的版本，而 HT$^{=n}_k$ 是 HT 限制为恰好 $n$ 个元素之和和 $k$ 种颜色的版本。甚至 HT$^{\leqslant 2}_2$ 似乎也是一个强原则，并且可能在 RCA$_0$ 下蕴涵 HT 本身。相比之下，已知 HT$^{=2}_2$ 在 RCA$_0$ 下严格弱于 HT，因为 HT$^{=2}_2$ 立即由对的二色 Ramsey 定理推出。事实上，HT$^{=2}_2$ 是否可计算地成立曾悬置数年。我们证明 HT$^{=2}_2$ 以及将加法替换为减法和其他运算的类似结果在 RCA$_0$ 甚至 WKL$_0$ 中不可证。事实上，我们证明存在 HT$^{=2}_2$ 的一个可计算实例，其所有解都能计算一个相对于 $\emptyset'$ 对角非可计算的函数。由此推出存在 HT$^{=2}_2$ 的一个可计算实例没有 $\Sigma^0_2$ 解，这是关于算术层次的最佳可能结果。此外，对前述关于相对于 $\emptyset'$ 为 DNC 的解的结果之证明的仔细分析表明，HT$^{=2}_2$ 在 RCA$_0$ 下蕴涵 RRT$^{=2}_2$，即对的二色彩虹 Ramsey 定理。我们如上构造可计算着色最有趣之处在于使用了 Rumyantsev 和 Shen 的 Lov\'asz 局部引理的有效版本。