An O((n center dot log n)(3))-time transformation from Grz into decidable fragments of classical first-order logic

The provability logic Grz is characterized by a class of modal frames that is not first-order definable. We present a simple embedding of Grz into dec idable fragments of classical first-order logic such as FO2 and the guarded fragment. The embedding is an O((n.log n)(3))-time transformation that nei ther involves first principles about Turing machines (and therefore is easy to implement), nor the semantical characterization of Grz (and therefore d oes not use any second-order machinery). Instead, we use the syntactic rela tionships between cut-free sequent-style calculi for Grz, S4 and T. We firs t translate Grz into T, and then we use the relational translation from T i nto FO2.