English

Turing jumps through provability

Logic 2015-01-23 v1

Abstract

Fixing some computably enumerable theory TT, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each Σ1\Sigma_1 formula is equivalent to some formula of the form Tφ\Box_T \varphi provided that TT is consistent. In this paper we give various generalizations of the FGH theorem. In particular, for n>1n>1 we relate Σn\Sigma_{n} formulas to provability statements [n]TTrueφ[n]_T^{\sf True}\varphi which are a formalization of "provable in TT together with all true Σn+1\Sigma_{n+1} sentences". As a corollary we conclude that each [n]TTrue[n]_T^{\sf True} is Σn+1\Sigma_{n+1}-complete. This observation yields us to consider a recursively defined hierarchy of provability predicates [n+1]T[n+1]^\Box_T which look a lot like [n+1]TTrue[n+1]_T^{\sf True} except that where [n+1]TTrue[n+1]_T^{\sf True} calls upon the oracle of all true Σn+2\Sigma_{n+2} sentences, the [n+1]T[n+1]^\Box_T recursively calls upon the oracle of all true sentences of the form nTϕ\langle n \rangle_T^\Box\phi. As such we obtain a `syntax-light' characterization of Σn+1\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[n+1]_T^\Box are well behaved in that together they provide a sound interpretation of the polymodal provability logic GLPω{\sf GLP}_\omega.

Keywords

Cite

@article{arxiv.1501.05327,
  title  = {Turing jumps through provability},
  author = {Joost J. Joosten},
  journal= {arXiv preprint arXiv:1501.05327},
  year   = {2015}
}
R2 v1 2026-06-22T08:09:05.022Z