Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
Ulrich Kohlenbach · Journal of Symbolic Logic · 1992
Abstract We show how to extract effective bounds Φ for ⋀ u 1 ⋀ v ≤ y tu ⋁ w η G 0 -sentences which depend on u only (i.e. ⋀ u ⋀ v ≤ y , tu ⋁ w ≤ η Φ u G 0 ) from arithmetical proofs which use analytical assumptions of the form ( ϒ, δ, ρ , and τ are arbitrary finite types, η ≤ 2, G 0 and F 0 are quantifier-free, and s and t are closed terms). If τ ≤ 2, (*) can be weakened to This is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.