2015/01/21 by Joost J. Joosten, Joosten, Joost J. · 2 citations
Computer Science · Mathematics · #Computability, Logic, AI Algorithms #Logic, Reasoning, and Knowledge #math.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1501.05327
arxiv created 2015/01/21 · arxiv updated 2015/01/23
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 \BoxT φ 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]^\BoxT 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]^\BoxT recursively calls upon the oracle of all true sentences of the form ⟨ n ⟩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ω.