Turing–Taylor Expansions for Arithmetic Theories

Abstract

Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories: iterate adding consistency of some weak base theory until you “hit” the target theory. Turing progressions based on n-consistency give rise to a ${\Pi_{n+1}}$ proof-theoretic ordinal ${|U|_{\Pi^0_{n+1}}}$ also denoted ${|U|_n}$. As such, to each theory U we can assign the sequence of corresponding ${\Pi_{n+1}}$ ordinals ${\langle |U|_n\rangle_{n > 0}}$. We call this sequence a Turing-Taylor expansion or spectrum of a theory. In this paper, we relate Turing-Taylor expansions of sub-theories of Peano Arithmetic to Ignatiev’s universal model for the closed fragment of the polymodal provability logic ${\mathsf{GLP}_\omega}$. In particular, we observe that each point in the Ignatiev model can be seen as Turing-Taylor expansions of formal mathematical theories. Moreover, each sub-theory of Peano Arithmetic that allows for a Turing-Taylor expansion will define a unique point in Ignatiev’s model.