
arXiv: 1106.5124
We study the logical and computational strength of weak compactness 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 $\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 ℓ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 [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.
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], FOS: Mathematics, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Mathematics - Logic, Logic (math.LO), 03F60 (Primary) 03D80, 03B30 (Secondary)
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], FOS: Mathematics, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], Mathematics - Logic, Logic (math.LO), 03F60 (Primary) 03D80, 03B30 (Secondary)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
