Title:A non-compact deduction rule for the logic of provability and its algebraic models

Abstract:In this paper, we introduce a proof system with a non-compact deduction rule, that is, a deduction rule with countably many premises, to axiomatize the logic $\mathbf{GL}$ of provability, and show its Kripke completeness in an algebraic manner. As $\mathbf{GL}$ is not canonical, a standard proof of Kripke completeness for $\mathbf{GL}$ is given by a Kripke model which is obtained by changing the binary relation of the canonical model, while our proof is given by a submodel of the canonical model of $\mathbf{GL}$ which is obtained by making use of an infinitary extension of the Jónsson-Tarski representation. We also show the three classes of algebras defined by $\Box x\leq\Box\Box x$ and one of the following three conditions, $\bigwedge_{n\in\omega}\Diamond^{n}1=0$, the non-compact deduction rule and the Löb formula, are mutually different, while all of them define $\mathbf{GL}$.