Local tabularity in MS4 with Casari's axiom

We study local tabularity (local finiteness) in some extensions of $\mathsf{M}\mathsf{S}\mathsf{4}$ (monadic $\mathsf{S}\mathsf{4}$). Our main result is a semantic characterization of local finiteness in varieties of ${\mathsf{M}}^{+}\mathsf{S}\mathsf{4}$-algebras, where ${\mathsf{M}}^{+}\mathsf{S}\mathsf{4}$ denotes the extension of $\mathsf{M}\mathsf{S}\mathsf{4}$ 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{S}\mathsf{4}[n]\times \mathsf{S}\mathsf{5}$ is an extension of ${\mathsf{M}}^{+}\mathsf{S}\mathsf{4}$, obtaining a criterion for extensions of $\mathsf{S}\mathsf{4}[n]\times \mathsf{S}\mathsf{5}$ as an application. Next, we give a characterization of local finiteness in varieties of $\mathsf{M}\mathsf{S}\mathsf{4}\mathsf{B}[2]$-algebras, where $\mathsf{M}\mathsf{S}\mathsf{4}\mathsf{B}$ denotes the extension of $\mathsf{M}\mathsf{S}\mathsf{4}$ by the Barcan axiom. We demonstrate that our methods cannot be extended beyond depth 2, as we give a translation of the fusion ${\mathsf{S}\mathsf{5}}_2$ into $\mathsf{M}\mathsf{S}\mathsf{4}\mathsf{B}[3]$ for $n\ge 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.