{
  "id": "1607.05237",
  "version": "v1",
  "published": "2016-07-18T18:46:14.000Z",
  "updated": "2016-07-18T18:46:14.000Z",
  "title": "A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem",
  "authors": [
    "Paulo Oliva",
    "Silvia Steila"
  ],
  "comment": "11 pages",
  "categories": [
    "math.LO"
  ],
  "abstract": "In 1979 Schwichtenberg showed that a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$ is closed under system $\\text{T}$. More precisely, if the functional $Y$ which controls the stopping condition of Spector's bar recursor is $\\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\\text{T}$-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for $\\alpha < \\varepsilon_0$ and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system $\\text{T}$ input, what the corresponding system $\\text{T}$ output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into $\\text{T}$-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if $Y$ is in the fragment $\\text{T}_i$ then terms built from $\\text{BR}^{\\mathbb{N}, \\sigma}$ for this particular $Y$ are definable in the fragment $\\text{T}_{i + \\max \\{ 1, \\text{level}(\\sigma) \\} + 2}$.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2016-07-18T18:46:14.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F07",
      "03F10"
    ],
    "keywords": [
      "schwichtenbergs bar recursion closure theorem",
      "direct proof",
      "rule-like version spectors bar recursion",
      "explicit construction"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 11,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}