Modal Logics that Bound the Circumference of Transitive Frames

TL;DR

This paper introduces a family of modal logics based on transitive frames with bounded cycle lengths, explores their axiomatizations, semantic properties, and topological interpretations, and analyzes their algebraic structures.

Contribution

It defines and axiomatizes new modal logics with bounded cycle lengths, studies their semantic and topological properties, and characterizes their algebraic models.

Findings

Each logic is decidable and has the finite model property.

The logics correspond to properties of hereditarily n+1-irresolvable spaces.

Modal algebras are generated by powerset algebras of finite frames with bounded cycles.

Abstract

For each natural number $n$ we study the modal logic determined by the class of transitive Kripke frames in which there are no cycles of length greater than $n$ and no strictly ascending chains. The case $n=0$ is the G\"odel-L\"ob provability logic. Each logic is axiomatised by adding a single axiom to K4, and is shown to have the finite model property and be decidable. We then consider a number of extensions of these logics, including restricting to reflexive frames to obtain a corresponding sequence of extensions of S4. When $n=1$, this gives the famous logic of Grzegorczyk, known as S4Grz, which is the strongest modal companion to intuitionistic propositional logic. A topological semantic analysis shows that the $n$-th member of the sequence of extensions of S4 is the logic of hereditarily $n+1$-irresolvable spaces when the modality $\Diamond$ is interpreted as the topological closure operation. We also study the definability of this class of spaces under the interpretation of $\Diamond$ as the derived set (of limit points) operation. The variety of modal algebras validating the $n$-th logic is shown to be generated by the powerset algebras of the finite frames with cycle length bounded by $n$. Moreover each algebra in the variety is a model of the universal theory of the finite ones, and so is embeddable into an ultraproduct of them.