A Proof Theory for Profinite Modal Algebras

TL;DR

This paper develops a proof-theoretic framework for profinite modal algebras, linking their algebraic properties with infinitary modal calculi and categorical regularity, advancing the understanding of their logical and algebraic structure.

Contribution

It introduces a modal calculus as a proof-theoretic presentation for profinite modal algebras and explores their categorical properties, bridging algebra, logic, and category theory.

Findings

Profinite $L$-algebras are monadic over Set.

Propositional theories in infinitary modal calculi can present profinite $L$-algebras.

Correspondences between syntactic calculus properties and categorical regularity/exactness.

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.