On the computational content of the Bolzano-Weierstraß Principle

DOI10.1002/MALQ.200910106zbMATH Open1209.03046OpenAlexW1964587127MaRDI QIDQ3053232FDOQ3053232

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Elimination of Skolem functions for monotone formulas in analysis
• Ü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 n-quantifier induction
• On the No-Counterexample Interpretation
• On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
• On Tao's “finitary” infinite pigeonhole principle
• Things that can and things that cannot be done in PRA

Cited In (10)

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

Recommendations

• On the Computational Content of the Brouwer Fixed Point Theorem 👍 👎
• On the computational content of Zorn's lemma 👍 👎
• The computational content of Walras' existence theorem 👍 👎
• Computability of Brolin-Lyubich measure 👍 👎
• A Computational Approach to the Borwein-Ditor Theorem 👍 👎
• COMPUTATIONAL ASPECTS OF HELLY’S THEOREM AND ITS RELATIVES 👍 👎
• Weihrauch Complexity in Computable Analysis 👍 👎
• Computable aspects of the Bachmann–Howard principle 👍 👎
• On the Computability of Blochs Constant 👍 👎
• Title not available (Why is that?) 👍 👎

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)