Turing Jumps Through Provability

Abstract: Fixing some computably enumerable theory

T

, the Friedman-Goldfarb-Harrington (FGH) theorem says that over elementary arithmetic, each

S i g m a_{1}

formula is equivalent to some formula of the form

B o x_{T} v a r p h i

provided that

T

is consistent. In this paper we give various generalizations of the FGH theorem. In particular, for

n > 1

we relate

S i g m a_{n}

formulas to provability statements

[n]_{T}^{s f T r u e} v a r p h i

which are a formalization of "provable in

T

together with all true

S i g m a_{n + 1}

sentences". As a corollary we conclude that each

[n]_{T}^{s f T r u e}

is

S i g m a_{n + 1}

-complete. This observation yields us to consider a recursively defined hierarchy of provability predicates

[n + 1]^{B} o x_{T}

which look a lot like

[n + 1]_{T}^{s f T r u e}

except that where

[n + 1]_{T}^{s f T r u e}

calls upon the oracle of all true

S i g m a_{n + 2}

sentences, the

[n + 1]^{B} o x_{T}

recursively calls upon the oracle of all true sentences of the form

l a n g l e n a n g l e_{T}^{B} o x p h i

. As such we obtain a `syntax-light' characterization of

S i g m a_{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}^{B} o x

are well behaved in that together they provide a sound interpretation of the polymodal provability logic

{s f G L P}_{o} m e g a

.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Turing Jumps Through Provability