Local tabularity in MS4 with Casari's axiom

TL;DR

This paper characterizes local finiteness in extensions of monadic S4 with Casari's and Barcan axioms, providing semantic and syntactic criteria, and explores the limits of these methods through translations and finite model properties.

Contribution

It offers a semantic and syntactic characterization of local finiteness in extended MS4 logics, and investigates the boundaries of these methods via translations and model properties.

Findings

Semantic characterization of local finiteness in M+S4 varieties.

Syntactic criterion via reducible path property for extensions.

Finite model property established for certain non-locally tabular logics.

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.