 Japaridze’s (1988) bimodal logic GLB has two \(\Box\)-like provability operators, denoted by \([0]\) and \([1]\), with their dual \(\Diamond\)-like operators \(\langle 0\rangle\) and \(\langle 1\rangle\), respectively. In Japaridze’s interpretation, one can think of \([0]\) as standing for the standard provability predicate in Peano Arithmetic. On the other hand, \([1]\) corresponds to a stronger provability predicate, namely \(\omega\)-provabilty. 