(Non-)well-founded derivations in the provability logic $\mathsf{GLP}$
Daniyar Shamkanov
TL;DR
This work investigates cyclic, non-well-founded, and well-founded infinitary derivations in the provability logic $\mathsf{GLP}$. It proves that cyclic derivations do not alter derivability and that the $\infty$-derivation and $\omega$-derivation frameworks yield the same infinitary extension, connecting these derivations to standard proofs. The authors develop robust algebraic and neighbourhood semantic frameworks (Magari algebras and Esakia frames) and establish strong local and global–local neighbourhood completeness for the infinitary extension, with a corresponding result for ordinary $\mathsf{GLP}$. They provide representation theorems showing Box-founded Magari algebras embed into powerset algebras of Esakia frames, and prove full neighbourhood completeness for the infinitary system, linking syntactic derivability with semantic entailment. Finally, they relate infinitary derivations to ordinary proofs by structural analyses of words and ground formulas, leveraging uniform interpolation and admissibility of an $\omega$-rule to translate infinitary reasoning into standard GLP proofs. The results deepen the understanding of GLP’s proof-theoretic and semantic structure and offer a unified view of infinitary derivations across algebraic and neighbourhood semantics.
Abstract
We examine cyclic, non-well-founded and well-founded derivations in the provability logic $\mathsf{GLP}$. While allowing cyclic derivations does not change the system, the non-well-founded and well-founded derivations we consider define the same proper infinitary extension of $\mathsf{GLP}$. We establish that this extension is strongly algebraic and neighbourhood complete with respect to both local and global semantic consequence relations. In fact, these completeness results are proved for generalizations of global and local consequence relations, which we call global-local. In addition, we prove strong local neighbourhood completeness for the original system $\mathsf{GLP}$ (with ordinary derivations only).