On provability logics with linearly ordered modalities (Q456968)

\textit{G. Japaridze} introduced polymodal provability logic {GLP} [Modal-logical means of studying provability. Moscow: Moscow State Univ. (Diss.) (1986)]. The language of {GLP} extends that of classical propositional logic by unary modalities [\(n\)], for each \(n\in \omega.\) The arithmetical interpretation of a formula \([n]\varphi\) is ``\(\varphi\) is provable from the axioms of Peano arithmetic together with all true arithmetical \(\Pi_n\)-sentences''. Roughly speaking, {GLP} grasps the modal properties of the formal arithmetic with the \(\omega\)-rule. Later, \textit{K. N. Ignatiev} [J. Symb. Log. 58, No. 1, 249--290 (1993; Zbl 0795.03082)] developed Japaridze's results about {GLP} for more general theories. The system {GLP} was used as a basis for a simple proof-theoretic analysis of Peano arithmetic [\textit{L. D. Beklemishev}, Ann. Pure Appl. Logic 128, No. 1--3, 103--123 (2004; Zbl 1048.03045)]. Beklemishev introduced the logics {GLP}\(_\Lambda\) in 2005 as a generalization of Japaridze's logic. If \(\Lambda\) is any linearly ordered set the Gödel-Löb logic {GLP}\(_\Lambda\) contains one modality \([\alpha]\) for each ordinal \(\alpha<\Lambda.\) Japaridze's system {GLP} is in fact the logic {GLP}\(_\omega.\) The system {GLP}\(_\Lambda\) has no non-trivial Kripke models, but \textit{K. N. Ignatiev} [Ann. Pure Appl. Logic 64, No. 1, 1--25 (1993; Zbl 0802.03014)] showed that its closed fragment {GLP}\(_\Lambda^0\) does. In the paper under review a normal form theorem for {GLP}\(_\Lambda^0\) is proved. Further, a restricted axiomatization of {GLP}\(_\Lambda^0\) is provided. At the end, the decidability of {GLP}\(_\Lambda^0\) for recursive orderings \(\Lambda\) is proved.