Well-founded orders on the transfinite Japaridze algebra II
David Fernández–Duque, Joost J. Joosten · arXiv (Cornell University) · 2012
The logic GLP is a polymodal logic that has for each ordinal \alpha an operator [\alpha ], whose intended interpretation is a provability predicate in a hierarchy of theories of increasing strength. Its corresponding algebra is called the (transfinite) Japaridze algebra. There are various natural orders in this algebra that are based on comparing consistency strength of its elements. In particular, for each \alpha we define A A. In this paper we shall consider worms, which are formulas of the form ... T, and the partial orders <_\alpha on their images in the Japaridze algebra. Given a worm A and an ordinal \alpha, our goal is to show how one computes the order type that is naturally associated to \Omega_\alpha(A):={B:B<_\alpha A}. Our main results show how the sequences can be computed via hyperations and cohyperations, which are forms of transfinite iterations of ordinal functions closely related to Veblen hierarchies.