 A polymodal analogue of Japaridze’s GLB, named GLP, has received a lot of attention in recent years. GLP has infinitely many \(\Box\)-like provability operators, denoted by boxes \([n]\) for every natural number \(n\), with their dual \(\Diamond\)-like operators \(\langle n\rangle\). Again, one can think of \([0]\) as standing for the standard provability predicate in Peano Arithmetic, \(\langle 1\rangle\) for \(\omega\)-provability, etcetera. GLP has been axiomatized by starting from the axioms and rules of GL (see  Section 2),  formulated separately for each \([n]\). In addition, GLP has three mixed axiom schemes, namely, as formulated by Beklemishev (2010):  \[ [m] A \rightarrow [n] A, \mbox{ for } m \leq n \]     \[ \langle k\rangle A \rightarrow [n]\langle k\rangle A, \mbox{ for } k \lt n \]     \[ [m] A \rightarrow [n][m] A, \mbox{ for } m \leq n \]   