An essentially algebraic glance to Kripke semantics: the S5 case

TL;DR

The paper addresses the dualization of finite $S5$-algebras through Gabriel–Ulmer duality, showing that finite $S5$-algebras classify an essentially algebraic theory whose models are Kan extensions of faithful actions of finite symmetric groups. It develops an intricate chain of equivalences: Ind-completions, Lex-presheaves, and finite Kripke frames yield a concrete description of the dual theory via first-order axioms $T_1$ and $T_2$, with the latter capturing the decomposition into canonical liftings of $S_m$-actions. The main result identifies the dual theory $T_2$ as being classified by the Lex-category $ ext{Lex}( ext{S5Fr}_{ ext{fin}}^{op}, ext{Set})$, and ties models to locally finite $S5$-Kripke frames and $p$-morphisms, thereby linking modal logic with finite-group combinatorics. This establishes a conceptual bridge between two areas and points to broader applicability to other logics and constraint-satisfaction phenomena.

Abstract

We show that the category of finite $\textit{S5}$-algebras (dual to finite reflexive, symmetric and transitive Kripke frames) classifies the essentially algebraic theory whose models are Kan extensions of faithful actions of the finite symmetric groups.

Theorems & Definitions (32)

• Example 1
• Example 2
• Example 3
• Example 4
• Theorem 2.1
• Definition 3.0.1
• Theorem 3.1
• Definition 3.1.1
• Theorem 3.2
• Theorem 3.3