On the Strength of Weak Compactness

We study the logical and computational strength of weak compactness in the separable Hilbert space ℓ₂.

Let weak-BW be the statement the every bounded sequence in ℓ₂ has a weak cluster point. It is known that weak-BW is equivalent to ACA₀ over RCA₀ and thus that it is equivalent to (nested uses of) the usual Bolzano-Weierstraß principle BW.

We show that weak-BW is instance-wise equivalent to $\Pi^0_2$ -CA. This means that for each $\Pi^0_2$ sentence A(n) there is a sequence $(x_i)_{i\in{\mathbb{N}}})$ in ℓ₂, such that one can define the comprehension function for A(n) recursively in a cluster point of (x_i)_i. As a consequence we obtain that the degrees d≥_T 0″ are exactly the degrees that contain a weak cluster point of any computable, bounded sequence in ℓ₂. Since a cluster point of any sequence in the unit interval [0,1] can be computed in a degree low over 0′ (see [10]), this also shows 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, cf. [7].

2010 Mathematics Subject Classification. Primary 03F60; Secondary 03D80, 03B30.