The reverse mathematics of the pigeonhole hierarchy
Quentin Le Houérou, Ludovic Levy Patey, Ahmed Mimouni
TL;DR
This work analyzes the infinite pigeonhole principle across the arithmetical hierarchy within $\\mathsf{RCA}_0$, proving the resulting hierarchy is strict and mapping its first-order consequences via sophisticated forcing methods. Central to the approach is iterated jump control, strengthened by forcing with trees, Scott towers, and largeness towers, to obtain low${}_{n+1}$ and weakly low${}_n$ bases for $\\Sigma^0_{n+1}-\\mathsf{Subset}$ and to preserve hyperimmunities. The authors establish $\\Pi^1_1$-conservativity results for these principles over suitable bases, connect the hierarchy to the Ginsburg–Sands theorem and cohesiveness, and derive ω-model separations between levels, contributing a broad, modular framework for the computational content of combinatorial theorems. The findings advance a program to understand the computational content of Ramsey-type results and their proof-theoretic strength, with implications for conservation and equivalence phenomena in reverse mathematics.
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.