Veblen hierarchy in the context of provability algebras
Lev D. Beklemishev · 2004
We study an extension of Japaridze’s polymodal logic GLP with transfinitely many modalities and develop a provability-algebraic ordinal notation system up to the ordinal Γ0. In the papers [1, 2] a new algebraic approach to the traditional prooftheoretic ordinal analysis was presented based on the concept of graded provability algebra. The graded provability algebra of a formal theory T is its Lindenbaum boolean algebra equipped with additional unary operators 〈n 〉 mapping a sentence ϕ to the sentence n-Con(ϕ) expressing that T + ϕ is n-consistent. The n-consistency operators, together with their dual n-provability operators, satisfy a particular modal logic GLP described by G. Japaridze (see [3]). In this framework, an ordinal notation system up to the ordinal ɛ0 naturally emerges from the closed fragment of GLP. This allows for a transparent proof-theoretic analysis of Peano arithmetic PA, including a characterization of its class of provably total computable functions and a consistency proof à la Gentzen. More