Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Exploring the computational contribution of a non-constructive combinatorial principle

Speaker: Trifon Trifonov
Author(s): Diana Ratiu and Trifon Trifonov
Slot: Array, 11:20-11:40, col. 2


The use of classical logic for some combinatoric proofs, as for
Ramsey's theorem or Weak K??ig's Lemma, can be localized in the
Infinite Pigeon Hole (IPH) principle, stating that any infinite
sequence, which is finitely colored, has an infinite monochromatic
subsequence. In general, there is no computable functional producing
such an infinite subsequence. However, it is possible to extract a
program from a corollary proving the classical existence of a finite
monochromatic subsequence of any given length. We applied two methods
for extraction from classical proofs - the refined A-translation, as
proposed by Berger et al., and G??el's Dialectica interpretation. In
this talk we will compare the resulting programs and indicate how
they reflect the computational content of IPH.

websites: Arnold Beckmann 2008-05-19