Local finiteness in varieties of MS4-algebras

It is a classic result of Segerberg and Maksimova that a variety of $\mathsf{S}\mathsf{4}$-algebras is locally finite iff it is of finite depth. Since the logic $\mathsf{M}\mathsf{S}\mathsf{4}$ (monadic $\mathsf{S}\mathsf{4}$) axiomatizes the one-variable fragment of $\mathsf{Q}\mathsf{S}\mathsf{4}$ (predicate $\mathsf{S}\mathsf{4}$), it is natural to try to generalize the Segerberg–Maksimova theorem to this setting. We obtain several results in this direction. Our positive results include the identification of the largest semisimple variety of $\mathsf{M}\mathsf{S}\mathsf{4}$-algebras. We prove that the corresponding logic $\mathsf{M}\mathsf{S}{\mathsf{4}}_{\mathsf{S}}$ has the finite model property. We show that both ${\mathsf{S}\mathsf{5}}^2$ and ${\mathsf{S}\mathsf{4}}_u$ are proper extensions of $\mathsf{M}\mathsf{S}{\mathsf{4}}_{\mathsf{S}}$, and that a direct generalization of the Segerberg–Maksimova theorem holds for a family of varieties containing the variety of ${\mathsf{S}\mathsf{4}}_u$-algebras. Our negative results include a translation of varieties of ${\mathsf{S}\mathsf{5}}_2$-algebras into varieties of $\mathsf{M}\mathsf{S}{\mathsf{4}}_{\mathsf{S}}$-algebras of depth 2, which preserves and reflects local finiteness. This, in particular, shows that the problem of characterizing locally finite varieties of $\mathsf{M}\mathsf{S}\mathsf{4}$-algebras (even of $\mathsf{M}\mathsf{S}{\mathsf{4}}_{\mathsf{S}}$-algebras) is at least as hard as that of characterizing locally finite varieties of ${\mathsf{S}\mathsf{5}}_2$-algebras – a problem that remains wide open.