On provability logics with linearly ordered modalities
  We introduce the logics GLP(\Lambda), a generalization of Japaridze's polymodal provability logic GLP(\omega) where \Lambda is any linearly ordered set representing a hierarchy of provability operators of increasing strength.   We shall provide a reduction of these logics to GLP(\omega) yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP(\Lambda) and the decidability of GLP(\Lambda) for recursive orderings \Lambda. Further, we give a restricted axiomatization of the variable-free fragment of GLP(\Lambda). 
Lev D. Beklemishev, David Fern\'andez-Duque, Joost J. Joosten
math.LO