ALL FINITELY AXIOMATIZABLE SUBFRAME LOGICS CONTAINING THE PROVABILITYLOGIC CSM0 ARE DECIDABLE

In this paper we investigate those extensions of the bimodal provabili ty logic CSM0 (alias PRL1 or F-) which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing CSM0 are de cidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with res pect to Kripke semantics.