We deal here with two modal logics, GL and Grz, that are known to have interesting arithmetical interpretations connected with the notion of provability. GL is the extensiom of K (or K4) by the schema □(□ A → A) → □ A, and Grz is the extension of S4 by □(□(A → □A) →A) → □A. GL is also known to be sound and complete with respect to the class of all Kripke models that are transitive, irreflexive and well founded. Grz bears the same relation to the corresponding reflexive models. We refer the reader to [1] for a full exposition of the subject. (See also [4], [2], [6].)In §I we develop a sequential calculus for both GL and Grz and give a semantical proof that both systems admit cut-elimination. (Incidentally, this provides an easy proof of the semantical completeness of the two systems.) With respect to GL this yields a correction of an error in [2].In §II we show that cut-elimination fails for QGL (the extension of GL to a language with quantifiers). We further show that, despite this failure, QGL still has some of GL's interesting properties (e.g., the disjunction property). We also show, using fixed-point techniques, that similar properties obtain if we take as semantics for QGL the arithmetical interpretation extended in the obvious way.We want to thank Professor H. Gaifman for his help while working on the subject.
Expressive power of existential first-order sentences of Büchi's sequential calculus
