Paper detail

Turing jumps through provability

Fixing some computably enumerable theory $T$, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each $Σ_1$ formula is equivalent to some formula of the form $\Box_T φ$ provided that $T$ is consistent. In this paper we give various generalizations of the FGH theorem. In particular, for $n>1$ we relate $Σ_{n}$ formulas to provability statements $[n]_T^{\sf True}φ$ which are a formalization of "provable in $T$ together with all true $Σ_{n+1}$ sentences". As a corollary we conclude that each $[n]_T^{\sf True}$ is $Σ_{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 $Σ_{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ϕ$. As such we obtain a `syntax-light' characterization of $Σ_{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}_ω$.