Lev Beklemishev based a novel paradigm for ordinal analysis of formal theories on calculations performed in the closed fragment of poly-modal provability logics. He used GLP to carry out $\Pi_n^0$ ordinal analyses of Peano Arithmetic (PA) and subsystems. GLP used $\omega$ many modalities. For theories beyond PA it is natural to work with transfinitely many modalities. The arising logics are still decidable and the closed fragments actually allow a fairly easy decision procedure. Full GLP does not admit Kripke semantics. For the closed fragment however a universal model was given by Ignatiev. In this talk we present this model and discuss how to extend it to the setting with transfinitely many modalities.
http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint232.pdf
http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint240.pdf
http://www.illc.uva.nl/Publications/ResearchReports/MoL-2008-06.text.pdf