The modal logic of provability: cut-elimination (Q790809)

\textit{D. Leivant} [J. Symb. Logic 46, 531--538 (1981; Zbl 0464.03019)] outlined a cut-elimination procedure for the formulation of the provability logic GL based on the only modal rule \(X,\square X,\square A\to A/\square X\to \square A\). The author and \textit{G. Sambin} [J. Philos. Logic 11, 311--342 (1982; Zbl 0523.03014)] gave a model-theoretic proof of the cut-elimination theorem for this formulation. An example is presented in the paper under review showing that Leivant's procedure can go in a loop. An additional reduction step is defined and the termination of the new procedure is proved.