Valentini's cut-elimination for provability logic resolved (Q2890695)

As for the problem of syntactical cut elimination in a sequent-style formulation of provability modal logic GL, there have been given various versions by several authors for their formulations with different methods, respectively, where some of them seem to leave ambiguity for details, as can happen sometimes in a proof by the so-called Gentzen method. Among others, the first one was proposed by Leivant, to which, however, Valentini showed soon a counterexample as well as another proof for a system based on sequents of formula sets by featuring a triple induction with the third parameter called ``width'' in addition to the usual ``degree'' and ``height (rank)'' of Gentzen. Afterwards, Moen claimed that Valentini's algorithms either do not terminate when applied to a multiset formulation of the calculus with an explicit rule of contraction. On the other hand, in general, the original mix (multi-cut) elimination method by Gentzen has also been revisited rather recently from the viewpoint to analyze such a problem brought about by structural rules. In this paper, the authors explain that Valentini's proof is not sufficient for manipulating the contraction rule explicitly, and then reconstruct the argument on the setting of multiset sequents with weakening and contraction, which is indeed carried out affirmatively but not straightly because of the global aspect of the third parameter ``width''. By analyzing the hidden role of structural rules in the argument thus, it is pointed out that Moen's claim is not correct; as a matter of fact, the algorithms used by him are essentially the same as those of Leivant. The authors discuss also the possibility of adapting their cut-elimination procedure to other logics axiomatizable by formulas of a syntactically similar form to the Löb axiom of GL.