Exploring the Computational Content of the Infinite Pigeonhole Principle
Daniel Ratiu, Trifon Trifonov · Journal of Logic and Computation · 2010
The use of classical logic for some combinatorial proofs, as it is the case with Ramsey’s theorem, can be localized in the Infinite Pigeonhole (IPH) principle, stating that any infinite sequence which is finitely colored has an infinite monochromatic subsequence. Since in general there is no com-putable functional producing such an infinite subsequence, we consider a Π02-corollary, proving the classical existence of a finite monochromatic subsequence of any given length. In order to obtain a program from this proof, we apply two methods for extraction: the refined A-Translation, as proposed by Berger et al., and Gödel’s Dialectica interpretation. In this paper, we compare the resulting programs with respect to their behavior and complexity and indicate how they reflect the computational content of IPH. 1