This paper contains a careful derivation of principles of Interpretability Logic valid in extensions of I0+1.

In this paper we study 1. the frame-theory of certain bimodal provability logics involving the reflection principle and we study2. certain specific bimodal logics with a provability predicate for a subtheory of Peano arithmetic axiomatized by a non-standardly finite number of axioms.

Provability logics with many modal operators for progressions of theories obtained by iterating their consistency statements are introduced. The corresponding arithmetical completeness theorem is proved.