We adapt our light Dialectica interpretation to usual and light modal formulas (with universal quantification on boolean and natural variables) and prove it sound for a non-standard modal arithmetic based on Goedel's T and classical S4. The range of this light modal Dialectica is the usual (non-modal) classical Arithmetic in all finite types (with booleans); the propositional kernel of its domain is Boolean and not S4. The `heavy' modal Dialectica interpretation is a new technique, as it cannot be simulated within our previous light Dialectica. The synthesized functionals are at least as good as before, while the translation process is improved. Through our modal Dialectica, the existence of a realizer for the defining axiom of classical S5 reduces to the Drinking Principle (cf. Smullyan).

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