标题： 一种对有限模态代数的证明理论 显示英文标题

标题： A Proof Theory for Profinite Modal Algebras

摘要： 在以前的论文中，我们证明了有限生成元的模态代数种类$L$生成的有限元的概形$L$-代数在$\mathbf{Set}$上是单射的。 这个单射性结果表明，概形$L$-代数可以作为命题理论的Lindenbaum代数，这些理论是命题模态演算的无限版本。 在本文中，我们将这些演算识别为Maehara-Takeuti的序列演算$\mathbf{LK}$的无限扩展的模态增强。 我们还研究了这些演算的语法性质与概形$L$-代数的对偶范畴的正规性/精确性性质之间的对应关系。 显示英文摘要

摘要： 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.