A technique that makes purely syntactic cut-elimination work for the provability logic GL. GL's Loeb-style modal rule leaves the cut formula (the diagonal formula) present in both premise and conclusion, so the standard double induction on cut-formula complexity and derivation height does not terminate. Working in a nested-sequent calculus, the diagonal-formula-elimination subprocedure removes the diagonal formula from the premise before the problematic reduction, restoring an ordinary double-induction termination argument and yielding a modular, unambiguous cut-elimination proof.
The provability logic GL is the modal logic of formal provability: reading the box operator as 'A is provable in Peano arithmetic', GL extends the modal logic K with the Löb axiom box(box A -> A) -> …