Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Local tabularity in MS4 with Casari's axiom

Chase Meadors

TL;DR

The paper advances the study of local finiteness for monadic modal logics by providing a semantic characterization of local finiteness in the M^{+}S4 family, built on the Casari axiom, and a syntactic criterion via the reducible path property rp_m. It shows that local finiteness for subvarieties of M^{+}S4 coincides with finite depth and local finiteness of the bottom-layer variety V|_T, and it proves a rp_m-based criterion that applies to extensions such as S4[n]×S5 and to MS4B[2]. Additionally, it establishes the finite model property for certain bounded-depth MS4 subvarieties and investigates the limitations of depth-3 characterizations through a translation from S5_2 to MS4B[3]. The results significantly illuminate when these extensions are locally finite and provide decidability insights via minimal-depth subvarieties, contributing to a more natural and robust theory around M^{+}S4 and related 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.

Local tabularity in MS4 with Casari's axiom

TL;DR

The paper advances the study of local finiteness for monadic modal logics by providing a semantic characterization of local finiteness in the M^{+}S4 family, built on the Casari axiom, and a syntactic criterion via the reducible path property rp_m. It shows that local finiteness for subvarieties of M^{+}S4 coincides with finite depth and local finiteness of the bottom-layer variety V|_T, and it proves a rp_m-based criterion that applies to extensions such as S4[n]×S5 and to MS4B[2]. Additionally, it establishes the finite model property for certain bounded-depth MS4 subvarieties and investigates the limitations of depth-3 characterizations through a translation from S5_2 to MS4B[3]. The results significantly illuminate when these extensions are locally finite and provide decidability insights via minimal-depth subvarieties, contributing to a more natural and robust theory around M^{+}S4 and related logics.

Abstract

We study local tabularity (local finiteness) in some extensions of (monadic ). Our main result is a semantic characterization of local finiteness in varieties of -algebras, where denotes the extension of 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 is an extension of , obtaining a criterion for extensions of as an application. Next, we give a characterization of local finiteness in varieties of -algebras, where denotes the extension of by the Barcan axiom. We demonstrate that our methods cannot be extended beyond depth 2, as we give a translation of the fusion into for 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.

Paper Structure

This paper contains 15 sections, 39 theorems, 23 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. MS4, algebraic semantics, and duality
  4. Depth of MS4-frames and related notions
  5. The fmp for some subvarieties of MS4 of bounded depth
  6. The Casari axiom and M+S4
  7. The dual spaces of M+S4-algebras
  8. A semantic characterization of local finiteness
  9. A syntactic criterion for local finiteness
  10. Minimal varieties in M+S4
  11. Local finiteness in MS4B
  12. Local finiteness of MS4B[2]
  13. A translation of S52 into MS4B[3]
  14. Conclusion
  15. Acknolwedgements

Key Result

Theorem 2.9

The category of $\mathsf{MS4}$-algebras with homomorphisms and the category of descriptive $\mathsf{MS4}$-frames with $\mathsf{MS4}$-morphisms are dually equivalent.

Figures (4)

  • Figure 4.1: The arguments for both direction of \ref{['thm:cas-frame-condition']}.
  • Figure 5.1: The key situations in \ref{['lem:irreducible-path-construction']}. The dashed arrows are obtained by an appeal to the Barcan axiom (B), the $\mathsf{MS4}$-axiom (M), or the depth of $\mathfrak{F}$ (D). The choice of $x_{i+1}$ is depicted in blue.
  • Figure 5.2: The situation in the proof of \ref{['lem:ms4b2-non-simple-cas']}.
  • Figure 5.3: Constructing a $\mathsf{MS4B_S}[3]$-frame from an $\mathsf{S5}_2$-frame. In the $\mathsf{S5}_2$-frame on top, $E_1$-clusters are horizontal lines while $E_2$-clusters are blue vertical lines. In the $\mathsf{MS4B_S}[3]$-frame on the right, $R$-clusters are horizontal lines, proper $R$-arrows are drawn with arrowheads, and $E$-clusters are given by the blue rectangles.

Theorems & Definitions (105)

  • Definition 2.1: FS77
  • Remark 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Theorem 2.9
  • Remark 2.10
  • ...and 95 more