On the strength of weak compactness

TL;DR

This paper analyzes the logical and computational strength of weak compactness in the Hilbert space ll_2, revealing its equivalence to b2^0_2-CA and its implications for computability and reverse mathematics.

Contribution

It establishes the precise logical strength of weak compactness in ll_2, showing its equivalence to b2^0_2-CA and analyzing its computational consequences.

Findings

Weak-BW is equivalent to b2^0_2-CA over RCA_0.

Degrees greater than 0 contain weak cluster points for computable sequences.

Weak-BW is strictly stronger than BW in computational strength.

Abstract

We study the logical and computational strength of weak compactness in the separable Hilbert space \ell_2. Let weak-BW be the statement the every bounded sequence in \ell_2 has a weak cluster point. It is known that weak-BW is equivalent to ACA_0 over RCA_0 and thus that it is equivalent to (nested uses of) the usual Bolzano-Weierstra{\ss} principle BW. We show that weak-BW is instance-wise equivalent to the \Pi^0_2-CA. This means that for each \Pi^0_2 sentence A(n) there is a sequence (x_i) in \ell_2, such that one can define the comprehension functions for A(n) recursively in a cluster point of (x_i). As consequence we obtain that the Turing degrees d > 0" are exactly those degrees that contain a weak cluster point of any computable, bounded sequence in \ell_2. Since a cluster point of any sequence in the unit interval [0,1] can be computed in a degree low over 0', this show also that instances of weak-BW are strictly stronger than instances of BW. We also comment on the strength of weak-BW in the context of abstract Hilbert spaces in the sense of Kohlenbach and show that his construction of a solution for the functional interpretation of weak compactness is optimal.