{
  "id": "1501.05327",
  "version": "v1",
  "published": "2015-01-21T21:18:06.000Z",
  "updated": "2015-01-21T21:18:06.000Z",
  "title": "Turing jumps through provability",
  "authors": [
    "Joost J. Joosten"
  ],
  "categories": [
    "math.LO"
  ],
  "abstract": "Fixing some computably enumerable theory $T$, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each $\\Sigma_1$ formula is equivalent to some formula of the form $\\Box_T \\varphi$ provided that $T$ is consistent. In this paper we give various generalizations of the FGH theorem. In particular, for $n>1$ we relate $\\Sigma_{n}$ formulas to provability statements $[n]_T^{\\sf True}\\varphi$ which are a formalization of \"provable in $T$ together with all true $\\Sigma_{n+1}$ sentences\". As a corollary we conclude that each $[n]_T^{\\sf True}$ is $\\Sigma_{n+1}$-complete. This observation yields us to consider a recursively defined hierarchy of provability predicates $[n+1]^\\Box_T$ which look a lot like $[n+1]_T^{\\sf True}$ except that where $[n+1]_T^{\\sf True}$ calls upon the oracle of all true $\\Sigma_{n+2}$ sentences, the $[n+1]^\\Box_T$ recursively calls upon the oracle of all true sentences of the form $\\langle n \\rangle_T^\\Box\\phi$. As such we obtain a `syntax-light' characterization of $\\Sigma_{n+1}$ definability whence of Turing jumps which is readily extended beyond the finite. Moreover, we observe that the corresponding provability predicates $[n+1]_T^\\Box$ are well behaved in that together they provide a sound interpretation of the polymodal provability logic ${\\sf GLP}_\\omega$.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2015-01-21T21:18:06.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "turing jumps",
      "polymodal provability logic",
      "fgh theorem",
      "elementary arithmetic",
      "theorem says"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2015arXiv150105327J"
    }
  }
}