A course in bimodal provability logic

The aim of the present paper is twofold: first I am somewhat dissatisfied with current treatments of Bimodal Provability Logic: the models employed there are singled out by certain syntactical conditions, moreover they validate the logics under consideration only locally. In this paper I give a decent model- & frame-theory for these logics. Secondly I study the modal logic of subsystems of Peano Arithmetic whose axiom sets are bounded by non-standard numbers (to be specific: non-standard numbers specifiable as the smallest number satifying some A0-formula). These systems play a role in certain arguments concerning Relative Interpretability. Moreover the Arithmetical Completeness Theorem for these systems can be applied to characterize which formulas of the language of ordinary, 'unimodal', provability logic are E1 (modulo provable equivalence in Peano Arithmetic) under all arithmetical interpretations ..