We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for G\"odel-L\"ob provability logic. In particular, we consider Sambin and Valentini's sequent system GLseq, Shamkanov's non-wellfounded and cyclic sequent systems GL$\infty$ and GLcirc, Poggiolesi's tree-hypersequent system CSGL, and Negri's labeled sequent system G3GL. Shamkanov showed how to transform proofs between GLseq, GL$\infty$, and GLcirc, and Gor\'e and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for G\"odel-L\"ob provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GLseq and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GLseq, GL$\infty$, GLcirc, CSGL, G3GL, and LNGL while also giving (to the best of the author's knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.

翻译：本文证明了哥德尔-勒布可证性逻辑中几种主要矢列演算形式化体系之间的证明可互译性。具体而言，我们考察了Sambin与Valentini的矢列系统GLseq、Shamkanov的非良基与循环矢列系统GL$\infty$和GLcirc、Poggiolesi的树状超矢列系统CSGL，以及Negri的标记矢列系统G3GL。Shamkanov曾展示如何在GLseq、GL$\infty$和GLcirc之间转换证明，Goré与Ramanayake则展示了如何在CSGL与G3GL之间转换证明，然而前三个系统与后两个系统之间的证明转换机制始终是未解决的开放问题。我们通过将树状超矢列证明重构为末端活跃形式，并引入一种新颖的线性化技术将此类证明转换为线性嵌套矢列证明，从而解决了这一开放问题。由此我们获得了一种从树状超矢列系统提取线性嵌套矢列系统的新证明论工具，并首次为哥德尔-勒布可证性逻辑构建了无切割的线性嵌套矢列演算LNGL。我们展示了如何将LNGL中的证明转换为特定范式——该范式下证明以模态规则与局部规则应用的阶段形式重复出现，且可转换为GLseq与G3GL证明。这些新的语法转换方法，结合前述已有转换，在GLseq、GL$\infty$、GLcirc、CSGL、G3GL和LNGL之间建立了完整的证明论对应关系，同时（据作者所知）首次在结构性系统（即标记、树状超矢列与线性嵌套矢列系统）与循环矢列系统之间构建了构造性的证明映射。