Kripke Models of Transfinite Provability Logic.
David Fernández–Duque, Joost J. Joosten · 2012
For any ordinal Λ, we can define a polymodal logic GLPΛ, with a modality [ξ] for each ξ < Λ. These represent provability predicates of increasing strength. Although GLPΛ has no non-trivial Kripke frames, Ignatiev showed that indeed one can construct a universal Kripke frame for the variable-free fragment with natural number modalities, denoted GLP 0 ω. In this paper we show how to extend these constructions for arbitrary Λ. More generally, for each ordinals Θ, Λ we build a Kripke model I Θ Λ and show that GLP 0 Λ is sound for this structure. In our notation, Ignatiev’s original model becomes I ε0 ω.