The Bolzano-Weierstrass theorem is the jump of weak Kőnig's lemma (Q408156)

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. The 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. The main results of the paper are: {\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. \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. \end{itemize}}