The reverse mathematics of the pigeonhole hierarchy

TL;DR

This paper investigates the reverse mathematical strength of the infinite pigeonhole principle across different levels of the arithmetical hierarchy, revealing its strict hierarchy and implications for computability and proof theory.

Contribution

It establishes the strictness of the pigeonhole hierarchy over RCA_0 and explores its first-order consequences, advancing the understanding of its computational content.

Findings

Hierarchy is strict over RCA_0

Constructs an elaborate iterated jump control

Analyzes first-order consequences of the hierarchy

Abstract

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.