On the computational content of the Bolzano-Weierstraß Principle

DOI10.1002/malq.200910106zbMath1209.03046OpenAlexW1964587127MaRDI 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 interpretationproof mininghard analysismonotone functional interpretationsequential compactnesscomputable functionalscomputational contentBolzano-Weierstraß principleGödel functional interpretation

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50) Higher-type and set recursion theory (03D65)

Related Items (8)

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

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

This page was built for publication: On the computational content of the Bolzano-Weierstraß Principle