Well-orders in the transfinite Japaridze algebra

TL;DR

This paper generalizes well-orderings in transfinite provability logic algebras, introduces a calculus for their order-types using hyperations, and characterizes certain ordinal sequences related to worms.

Contribution

It extends Beklemishev's orderings and provides a new calculus for generalized order-types using hyperations and cohyperations.

Findings

Presented a generalized ordering $<_\xi$ on worms.

Developed a calculus for computing order-types $o_\xi$.

Characterized sequences of ordinals via hyperations and cohyperations.

Abstract

This paper studies the transfinite propositional provability logics $\glp_\Lambda$ and their corresponding algebras. These logics have for each ordinal $\xi< \Lambda$ a modality $\la \alpha \ra$. We will focus on the closed fragment of $\glp_\Lambda$ (i.e., where no propositional variables occur) and \emph{worms} therein. Worms are iterated consistency expressions of the form $\la \xi_n\ra \ldots \la \xi_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}_\xi (A) \ra_{\xi \in \ord}$ for some worm $A$. One of these characterizations is in terms of a second kind of transfinite iteration called {\em cohyperation.}