A Proof Theory for Profinite Modal Algebras
Matteo De Berardinis, Silvio Ghilardi
TL;DR
The paper develops an infinitary proof-theoretic framework to present profinite modal $L$-algebras, leveraging the monadic description of these algebras over $ extbf{Set}$ and a Lindenbaum construction that ties infinitary propositional modal calculi to algebraic structure. It identifies the calculi as modal enrichments of Maehara-Takeuti's infinitary extension of the sequent calculus and uses dualities with locally finite Kripke frames to relate syntactic properties (Beth definability, Craig interpolation) to regularity/exactness properties in the dual category, via factorization systems. It provides detailed characterizations linking perfect algebraic properties to logical definability and interpolation phenomena, and contrasts the infinitary setting with the finitary one, noting simplifications and new phenomena (e.g., epis being regular for logics extending $K4$). The work also outlines open problems, including a complete infinitary cut-elimination program and a proposed sequent calculus for infinitary normal modal logic $K$, linking proof theory with categorical semantics for profinite structures.
Abstract
In a previous paper, we showed that profinite $L$-algebras (where $L$ is a variety of modal algebras generated by its finite members) are monadic over $\mathbf{Set}$. This monadicity result suggests that profinite $L$-algebras could be presented as Lindenbaum algebras for propositional theories in infinitary versions of propositional modal calculi. In this paper we identify such calculi as modal enrichments of Maehara-Takeuti's infinitary extension of the sequent calculus $\mathbf{LK}$. We also investigate correspondences between syntactic properties of the calculi and regularity/exactness properties of the opposite category of profinite $L$-algebras.