关于弱紧的强度
On the strength of weak compactness
摘要：
研究了可分希尔伯特空间\ell_2中弱紧的逻辑强度和计算强度.设弱BW是\ell_2中每个有界序列都有弱聚点的命题。已知弱BW等价于RCA_0上的ACA_0，因此它等价于通常的Bolzano-Weierstraße原理BW（嵌套使用）。我们证明了弱BW与弱0_2-CA在实例上是等价的。这意味着，对于每个\ell_2，A（n）中有一个序列（x_i），因此可以在（x_i）的聚类点中递归地定义A（n）的理解函数。因此我们得到图灵度d > 0”恰好是包含\ell_2中任何可计算有界序列的弱聚点的那些度。由于单位区间[0，1]中任何序列的聚类点都可以以低于0 '的程度计算，这也表明弱BW的实例严格强于BW的实例。我们还评论的强度弱BW的背景下，抽象的希尔伯特空间的意义上的Kohlenbach，并表明他的建设的解决方案的功能解释的弱紧是最佳的。
英文摘要：
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ß principle BW. We show that weak-BW is instance-wise equivalent to the Π^0_2-CA. This means that for each Π^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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
