Turing Jumps Through Provability

Abstract

Fixing some computably enumerable theory $T$, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each ${\varSigma }_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 ${\varSigma }_{n}$ formulas to provability statements $[n]^{\mathsf{True}}_T\varphi$ which are a formalization of “provable in $T$ together with all true ${\varSigma }_{n+1}$ sentences”. As a corollary we conclude that each $[n]^{\mathsf{True}}_T$ is ${\varSigma }_{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]^{\mathsf{True}}_T$ except that where $[n+1]^{\mathsf{True}}_T$ calls upon the oracle of all true ${\varSigma }_{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 ${\varSigma }_{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 ${\mathsf {GLP}} _\omega$.