{
  "id": "1106.5124",
  "version": "v1",
  "published": "2011-06-25T13:02:46.000Z",
  "updated": "2011-06-25T13:02:46.000Z",
  "title": "On the strength of weak compactness",
  "authors": [
    "Alexander P. Kreuzer"
  ],
  "journal": "Computability, vol. 1 (2012), no. 2, 171-179",
  "doi": "10.3233/COM-12010",
  "categories": [
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2011-06-25T13:02:46.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F60",
      "03D80",
      "03B30"
    ],
    "keywords": [
      "weak compactness",
      "weak cluster point",
      "bounded sequence",
      "equivalent",
      "abstract hilbert spaces"
    ],
    "tags": [
      "journal article"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2011arXiv1106.5124K"
    }
  }
}