On the computational content of the Bolzano-Weierstraß Principle
Pavol Safarik, Ulrich Kohlenbach · Mathematical logic quarterly · 2010
We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation (combined with negative translation) as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] (with the standard product metric). This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied to fixed sequences in Πi ∈ℕ[–ki, ki] (© 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)