Tue, 27 Feb 2024, 1:25 pm MT
$\textrm{S}4$-algebras (or interior algebras) provide semantics for the well-known modal logic $\textrm{S}4$, and there is a syntactic criterion characterizing when a variety of $\textrm{S}4$-algebras is locally finite in terms of its ``depth'' (a classical result of Segerberg and Maksimova). Since the logic $\textrm{MS}4$ (monadic $\textrm{S}4$) axiomatizes the one-variable fragment of predicate $\textrm{S}4$, it is natural to try to generalize the Segerberg$-$Maksimova theorem to this setting. We discuss several results in this direction. We establish that this theorem naturally extends to a family of subvarieties of $\textrm{MS}4$ containing, in particular, $\textrm{S}4_u$ ($\textrm{S}4$ with a universal modality). On the other hand, we provide a translation of varieties of $\textrm{S}5_2$-algebras into varieties of $\textrm{MS}4$-algebras of depth $2$ which preserves and reflects local finiteness, demonstrating that the problem of characterizing locally finite varieties of $\textrm{MS}4$-algebras is at least as hard as the corresponding problem for $\textrm{S}5_2$ (the bimodal logic of two unrelated $\textrm{S}5$ modalities), a wide-open problem. Finally, we discuss another natural subvariety of $\textrm{MS}4$ obtained by asserting a monadic analogue of Casari's predicate formula; this subvariety plays a role in obtaining a faithful provability interpretation of monadic intuitionistic predicate logic, and is expected to have a more manageable characterization of local finiteness.