Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization

DOI10.2307/2275367zbMath0781.03051OpenAlexW2004219814MaRDI QIDQ4032661

Ulrich Kohlenbach

Publication date: 1 April 1993

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2275367

zbMATH Keywords

weak König's lemmafunctional interpretationextraction of bounds

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50)

Related Items (23)

Proof mining in \(L_{1}\)-approximation ⋮ Light monotone Dialectica methods for proof mining ⋮ Term extraction and Ramsey's theorem for pairs ⋮ New effective moduli of uniqueness and uniform a priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory ⋮ Bounded functional interpretation and feasible analysis ⋮ A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC ⋮ Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic ⋮ On computational properties of Cauchy problems generated by accretive operators ⋮ Primitive recursion and the chain antichain principle ⋮ Unnamed Item ⋮ Things that can and things that cannot be done in PRA ⋮ Harrington's conservation theorem redone ⋮ Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation ⋮ Bounded functional interpretation ⋮ A complexity analysis of functional interpretations ⋮ Uniform Heyting arithmetic ⋮ Strongly uniform bounds from semi-constructive proofs ⋮ On the computational content of the Bolzano-Weierstraß Principle ⋮ A Clausal Approach to Proof Analysis in Second-Order Logic ⋮ On uniform weak König's lemma ⋮ THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT ⋮ Classical provability of uniform versions and intuitionistic provability ⋮ Pointwise hereditary majorization and some applications

Cites Work

• Unnamed Item
• Unnamed Item
• Fragments of arithmetic
• Pointwise hereditary majorization and some applications
• A constructive development of Chebyshev approximation theory
• On some formalized conservation results in arithmetic
• Remarks on Herbrand normal forms and Herbrand realizations
• Herbrand analyses
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Some models for intuitionistic finite type arithmetic with fan functional
• A relative consistency proof

This page was built for publication: Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization