Completeness of logics with the transitive closure modality and related logics

TL;DR

This paper establishes a sufficient condition called definable filtration (ADF) for the Kripke completeness of modal logics with transitive closure, ensuring finite model property and applicability to PDL-like expansions.

Contribution

It introduces the ADF condition as a new criterion for completeness and finite model property in extended modal logics with transitive closure.

Findings

Logic admits ADF implies completeness and finite model property.

The ADF condition can be iterated for multiple expansions.

Finite model property established for PDL-like expansions with ADF.

Abstract

We give a sufficient condition for Kripke completeness of modal logics enriched with the transitive closure modality. More precisely, we show that if a logic admits what we call definable filtration (ADF), then such an expansion of the logic is complete; in addition, has the finite model property, and again ADF. This argument can be iterated, and as an application we obtain the finite model property for PDL-like expansions of logics that ADF.