The infinite pigeonhole principle for $k$ colors ($\mathsf{RT}_k$) states, for every $k$-partition $A_0 \sqcup \dots \sqcup A_{k-1} = \mathbb{N}$, the existence of an infinite subset~$H \subseteq A_i$ for some~$i < k$. This seemingly trivial combinatorial principle constitutes the basis of Ramsey's theory, and plays a very important role in computability and proof theory. In this article, we study the infinite pigeonhole principle at various levels of the arithmetical hierarchy from both a computability-theoretic and reverse mathematical viewpoint. We prove that this hierarchy is strict over~$\mathsf{RCA}_0$ using an elaborate iterated jump control construction, and study its first-order consequences. This is part of a large meta-mathematical program studying the computational content of combinatorial theorems.
翻译:$k$色无限鸽巢原理($\mathsf{RT}_k$)断言:对于任意$k$划分$A_0 \sqcup \dots \sqcup A_{k-1} = \mathbb{N}$,总存在某个$i < k$使得$A_i$包含无限子集$H \subseteq A_i$。这一看似平凡的组合原理构成了拉姆齐理论的基石,并在可计算性与证明论中扮演着重要角色。本文从可计算性理论与逆数学的双重视角,研究算术层级不同阶上的无限鸽巢原理。通过精心设计的迭代跃迁控制构造,我们证明了该层级在$\mathsf{RCA}_0$系统上是严格的,并考察了其一阶逻辑推论。此项研究隶属于探究组合定理计算内涵的大型元数学计划。