 Japaridze’s bimodal provability logic GLB can be axiomatized by the axioms and rules of GL (see  Section 2),  formulated separately for [0] and [1]. In addition, GLB has two mixed axioms, namely:   \[\tag{Monotonicity} [0] A \rightarrow [1] A \]     \[\tag{\(\Pi^0_1\)-completeness} \langle 0\rangle A \rightarrow [1]\langle 0\rangle A \]   Japaridze’s logic is decidable and has a reasonable Kripke semantics, and it is arithmetically sound and complete with respect to Peano Arithmetic (Japaridze 1988, Boolos 1993).