The author deals with two modal logics, GL and Grz, that are known to have interesting arithmetical interpretations connected with the notion of provability. GL [Grz] is the extension of K [S4] by the schema \(\square (\square A\to A)\to \square A\) [\(\square (\square (A\to \square A)\to A)\to \square A]\). In § I he develops a sequential calculus for GL and Grz, and gives a semantical proof that both systems admit cut- elimination. In § II he shows that cut-elimination fails for QGL which is the extension of GL to a language with quantifiers. He further shows that, despite this failure, QGL still has some of GL’s interesting properties, e.g. disjunction property. He also shows, using fixed-point techniques, that similar properties are obtained if we take as semantics for QGL the arithmetical interpretation extended in the obvious way.