Flat modal fixpoint logics with the converse modality

TL;DR

This paper establishes a generic completeness result for flat modal fixpoint logics with the converse modality, extending previous work and introducing a new proof technique that constructs models directly.

Contribution

It extends completeness results to flat modal fixpoint logics with the converse modality and introduces a novel model construction approach using the induction rule.

Findings

Completeness proof for flat modal fixpoint logics with converse modality.

New model construction method using induction rule.

Extension of previous results by Santocanale and Venema.

Abstract

We prove a generic completeness result for a class of modal fixpoint logics corresponding to flat fragments of the two-way mu-calculus, extending earlier work by Santocanale and Venema. We observe that Santocanale and Venema's proof that least fixpoints in the Lindenbaum-Tarski algebra of certain flat fixpoint logics are constructive, using finitary adjoints, no longer works when the converse modality is introduced. Instead, our completeness proof directly constructs a model for a consistent formula, using the induction rule in a way that is similar to the standard completeness proof for propositional dynamic logic. This approach is combined with the concept of a focus, which has previously been used in tableau based reasoning for modal fixpoint logics.