On the computational content of the Bolzano-Weierstraß Principle
From MaRDI portal
Publication:3053232
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
Dialectica interpretation; proof mining; hard analysis; monotone functional interpretation; sequential compactness; computable functionals; computational content; Bolzano-Weierstraß principle; Gödel functional interpretation
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