On the computational content of the Bolzano-Weierstraß Principle

DOI10.1002/malq.200910106zbMath1209.03046MaRDI QIDQ3053232

Pavol Safarik, Ulrich Kohlenbach

Publication date: 4 November 2010

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.200910106

zbMATH Keywords

Dialectica interpretation; proof mining; hard analysis; monotone functional interpretation; sequential compactness; computable functionals; computational content; Bolzano-Weierstraß principle; Gödel functional interpretation

Mathematics Subject Classification ID

03F60: Constructive and recursive analysis

03F10: Functionals in proof theory

03F50: Metamathematics of constructive systems

03D65: Higher-type and set recursion theory

Related Items

A note on the finitization of Abelian and Tauberian theorems, The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma, Gödel functional interpretation and weak compactness, On quantitative versions of theorems due to F. E. Browder and R. Wittmann, Term extraction and Ramsey's theorem for pairs, The cohesive principle and the Bolzano-Weierstraß principle, A note on the monotone functional interpretation, A UNIFORM QUANTITATIVE FORM OF SEQUENTIAL WEAK COMPACTNESS AND BAILLON'S NONLINEAR ERGODIC THEOREM

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Elimination of Skolem functions for monotone formulas in analysis
• On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
• Things that can and things that cannot be done in PRA
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• Ordinal analysis of simple cases of bar recursion
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• On the No-Counterexample Interpretation
• On Tao's “finitary” infinite pigeonhole principle
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• On n-quantifier induction