Well-orders in the transfinite Japaridze algebra II: Turing progressions and their well-orders

TL;DR

This paper explores the structure of transfinite extensions of Japaridze's provability logic GLP, focusing on the well-founded partial orders induced by ordinals and their implications for modal semantics and Turing progressions.

Contribution

It introduces the analysis of unrestricted, well-founded partial orders in transfinite GLP, extending previous work on linear orders and impacting modal semantics and Turing progressions.

Findings

Unrestricted partial orders are well-founded but not linear.

These orders influence the semantics of GLP.

Implications for Turing progressions are significant.

Abstract

We study transfinite extensions of Japaridze's provability logic GLP and the well-founded relations that naturally occur within them. Every ordinal induces a partial order over the class of "words," which are iterated consistency statements expressible within GLP. Well-ordered restrictions of these partial orders have been studied previously; in this paper we consider the unrestricted partial orders, which are no longer linear but remain well-founded. These unrestricted partial orders bear important repercussions on modal semantics for GLP and on Turing progressions.