Local tabularity in MS4 with Casari's axiom

Abstract

We study local tabularity (local finiteness) in some extensions of $\mathsf{MS4}$ (monadic $\mathsf{S4}$). Our main result is a semantic characterization of local finiteness in varieties of $\mathsf{M^{+}S4}$-algebras, where $\mathsf{M^{+}S4}$ denotes the extension of $\mathsf{MS4}$ by the Casari axiom. We improve this to a syntactic criterion via the reducible path property identified in [Shap16], and note that the product logic $\mathsf{S4}[n] \times \mathsf{S5}$ is an extension of $\mathsf{M^{+}S4}$, obtaining a criterion for extensions of $\mathsf{S4}[n] \times \mathsf{S5}$ as an application. Next, we give a characterization of local finiteness in varieties of $\mathsf{MS4B}[2]$-algebras, where $\mathsf{MS4B}$ denotes the extension of $\mathsf{MS4}$ by the Barcan axiom. We demonstrate that our methods cannot be extended beyond depth 2, as we give a translation of the fusion $\mathsf{S5}_2$ into $\mathsf{MS4B}[3]$ for $n \geq 3$ that preserves and reflects local finiteness, suggesting that a characterization there remains difficult. Finally, we also establish the finite model property for some of these logics which are not known to be locally tabular.