Polynomial-time algorithms from ineffective proofs

We present a constructive procedure for extracting polynomial-time realizers from ineffective proofs of Π₂⁰-theorems in feasible analysis. By ineffective proof we mean a proof which involves the noncomputational principle weak Konig´s lemma WKL, and by feasible analysis we mean Cook and Urquhart´s system CPV^ω plus quantifier-free choice QF-AC. We shall also discuss the relation between the system CPV^ω + QF-AC and Ferreira´s base theory for feasible analysis BTFA, for which Π₂⁰-conservation of WKL has been non-constructively proven. This paper treats the case of weak Konig´s lemma, we indicate how to formalize the proof of the Heine/Borel covering lemma in this system. The main techniques used in the paper are Godel´s functional interpretation and a novel form of binary bar recursion.