1 ON THE STRENGTH OF WEAK COMPACTNESS
Alexander P. Kreuzer · 2015
Abstract. We study the logical and computational strength of weak com-pactness in the separable Hilbert space `2. Let weak-BW be the statement the every bounded sequence in `2 has a weak cluster point. It is known that weak-BW is equivalent to ACA0 over RCA0 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 Π02-CA. This means that for each Π02 sentence A(n) there is a sequence (xi)i∈N in `2, such that one can define the comprehension function for A(n) recursively in a cluster point of (xi)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 `2. Since a cluster point of any sequence in the unit interval [0, 1] can be computed in a degree low over 0 ′ (see [Kre11]), this also shows that instances of weak-BW are strictly stronger than instances of BW. 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. [Koh]. We investigate the computational and logical strength of weak sequential com-pactness in the separable Hilbert space `2. The strength of weak compactness has so far only been studied in the context of proof mining where general Hilbert spaces in a more general logical system are considered, see [Koh10, Koh]. It is straightforward to deduce from this analysis that weak compactness for `2 is equivalent to ACA0 over RCA0. In this paper we refine this result and show that weak compactness on `2 is instance-wise equivalent to Π02-CA over RCA0. This means that for each bounded sequence in `2 one can uniformly compute a function f such that from a compre-hension function for ∀x∃y f(x, y, n) = 0 one can compute a weak cluster point of the sequence and vice versa. As a consequence we obtain that the degrees d ≥T 0′ ′ are exactly the degrees that compute a weak cluster point for each computable bounded sequence in `2 and that there is a computable bounded sequence in `2 such that from any cluster point of this sequence one can compute 0′′.