The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma
type: Item
instance of: scholarly article
title: The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma
zbMATH Open document ID: 1245.03097
author: Vasco Brattka
author: Guido Gherardi
author: Alberto Marcone
published in: Annals of Pure and Applied Logic
publication date: 2012-03-29T00:00:00Z
full work available at URL: https://arxiv.org/abs/1101.0792
reviewed by: Iris Loeb
Mathematics Subject Classification ID: 03F60
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03D30
Mathematics Subject Classification ID: 03E15
zbMATH DE Number: 6019353
zbMATH Keywords: computable analysis
zbMATH Keywords: constructive analysis
zbMATH Keywords: reverse mathematics
zbMATH Keywords: effective descriptive set theory
zbMATH Keywords: Bolzano-Weierstraß theorem
zbMATH Keywords: jump in the Weihrauch lattice
zbMATH Keywords: weak König's lemma
MaRDI profile type: Publication
Wikidata QID: Q124965796
OpenAlex ID: W2018837422
arXiv ID: 1101.0792
cites work: A fan-theoretic equivalent of the antithesis of Specker's theorem
cites work: Computable invariance
cites work: Effective Borel measurability and reducibility of functions
cites work: On Computable Compact Operators on Banach Spaces
cites work: Borel complexity and computability of the Hahn-Banach theorem
cites work: Borel Complexity of Topological Operations on Computable Metric Spaces
cites work: Effective Choice and Boundedness Principles in Computable Analysis
cites work: Weihrauch degrees, omniscience principles and weak computability
cites work: Computability on subsets of metric spaces.
cites work: Closed choice and a uniform low basis theorem
cites work: Constructive notions of equicontinuity
cites work: Q3994935
cites work: How incomputable is the separable Hahn-Banach theorem?
cites work: Complexity Issues for Preorders on Finite Labeled Forests
cites work: Q5718575
cites work: ∏ 0 1 Classes and Degrees of Theories
cites work: Q4323294
cites work: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
cites work: On the Strength of Weak Compactness
cites work: The cohesive principle and the Bolzano-Weierstraß principle
cites work: Undecidability in Weihrauch Degrees
cites work: Singular coverings and non‐uniform notions of closed set computability
cites work: Limited Omniscience and the Bolzano-Weierstrass Principle
cites work: Q3611832
cites work: Classical recursion theory. The theory of functions and sets of natural numbers
cites work: How discontinuous is computing Nash equilibria? (Extended abstract)
cites work: Q3075220
cites work: On the (semi)lattices induced by continuous reducibilities
cites work: On the computational content of the Bolzano-Weierstraß Principle
cites work: Q4220572
cites work: Q4040892
cites work: Automata, Languages and Programming
cites work: Q4485693
cites work: Computational complexity on computable metric spaces
cites work: Revising Type-2 Computation and Degrees of Discontinuity
DOI: 10.1016/J.APAL.2011.10.006
review text: In this paper the computational content of the Bolzano-Weierstraß theorem and variants thereof are investigated. This is done by interpreting these theorems as partial multi-valued functions and placing them in the Weihrauch lattice.NEWLINENEWLINEThe authors start by proving basic properties of the Weihrauch lattice, and discussing closed choice and omniscience principles, compositional products, and derivatives (or: jumps) of a Weihrauch degree. Next they present their results on the Bolzano-Weierstraß theorem and the cluster-point problem. Finally, these results are compared with related results in computable analysis, constructive analysis (e.g., on the antithesis of Specker's theorem), reverse mathematics, and proof theory.NEWLINENEWLINEThe main results of the paper are:NEWLINE{\parindent=5mm \begin{itemize} \item[1.] The derivative of closed choice of a computable metric space is the cluster-point problem.\item [2.] The Bolzano-Weierstraß theorem can be characterized as the derivative of compact choice:{\parindent=8mm \begin{itemize}\item[*] The Bolzano-Weierstraß theorem on real numbers is the jump of weak König's lemma.\item [*] The Bolzano-Weierstraß theorem on the binary space is the jump of LLPO.\item [*] The Bolzano-Weierstraß theorem on natural numbers is the jump of the idempotent closure of LLPO.NEWLINENEWLINE\end{itemize}} \item [3.] The Bolzano-Weierstraß theorem is the compositional product of weak König's lemma and the monotone convergence theorem.\item [4.] The Bolzano-Weierstraß theorem on real numbers is complete for the class of weakly limit-computable functions.\item [5.] The unique-cluster-point problem on real numbers is complete for the class of functions that are limit-computable with finitely many mind changes.\item [6.] The Bolzano-Weierstraß theorem on real numbers and, more generally, the unbounded-cluster-point theorem on real numbers are uniformly low-limit-computable.NEWLINENEWLINE\end{itemize}}
description: scientific article; zbMATH DE number 6019353