Well-orders in the transfinite Japaridze algebra

Abstract

This paper studies the transfinite propositional provability logics $\glp_Λ$ and their corresponding algebras. These logics have for each ordinal $\xi <\Lambda$ a modality $\la α\ra$. We will focus on the closed fragment of $\glp_Λ$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la ξ_n\ra \ldots \la ξ_1 \ra \top$. Beklemishev has defined well-orderings ${<}_{\xi }$ on worms whose modalities are all at least $\xi$ and presented a calculus to compute the respective order-types. In the current paper we present a generalization of the original ${<}_{\xi }$ orderings and provide a calculus for the corresponding generalized order-types $o_{\xi }$. Our calculus is based on so-called {\em hyperations} which are transfinite iterations of normal functions. Finally, we give two different characterizations of those sequences of ordinals which are of the form $\la {\formerOmega}_ξ(A) \ra_{ξ\in \ord}$ for some worm $A$. One of these characterizations is in terms of a second kind of transfinite iteration called {\em cohyperation.}

Corrected a minor but confusing omission in the relation between Veblen progressions and hyperations