On the computational content of the Bolzano-Weierstraß Principle

DOI10.1002/MALQ.200910106MaRDI QIDQ3053232zbMATH OpenOpenAlexFDO

Authors 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

proof mininghard analysisDialectica interpretationmonotone functional interpretationsequential compactnesscomputable functionalscomputational contentBolzano-Weierstraß principleGödel functional interpretation

Mathematics Subject Classification ID

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

Recommendations

• The computational content of Walras' existence theorem
• A computational approach to the Borwein-Ditor theorem
• On the computational content of the Brouwer fixed point theorem
• Computable aspects of the Bachmann-Howard principle
• On the computational content of Zorn's lemma
• Weihrauch Complexity in Computable Analysis
• COMPUTATIONAL ASPECTS OF HELLY’S THEOREM AND ITS RELATIVES
• On the Computability of Blochs Constant
• Computability of Brolin-Lyubich measure
• Some computational aspects of Helly-type theorems

Cites work

• scientific article; zbMATH DE number 3504946 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 1222925 (Why is no real title available?)
• scientific article; zbMATH DE number 2174396 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3335898 (Why is no real title available?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Elimination of Skolem functions for monotone formulas in analysis
• On n-quantifier induction
• On Tao's “finitary” infinite pigeonhole principle
• On the No-Counterexample Interpretation
• On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
• On the logical analysis of proofs based on nonseparable Hilbert space theory
• Ordinal analysis of simple cases of bar recursion
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• Things that can and things that cannot be done in PRA
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(15)

• The Bolzano-Weierstrass theorem and set-theory
• On the computational content of Zorn's lemma
• The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma
• The cohesive principle and the Bolzano-Weierstraß principle
• The computational content of Walras' existence theorem
• On quantitative versions of theorems due to F. E. Browder and R. Wittmann
• Term extraction and Ramsey's theorem for pairs
• Gödel functional interpretation and weak compactness
• A uniform quantitative form of sequential weak compactness and Baillon's nonlinear ergodic theorem
• A note on the monotone functional interpretation
• Proof mining and combinatorics. Program extraction for Ramsey's theorem for pairs
• Addendum to: ``The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma
• The computational content of nonstandard analysis
• The computational significance of Hausdorff's maximal chain principle
• A note on the finitization of Abelian and Tauberian theorems

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3053232)