Completeness for flat modal fixpoint logics

This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set Γ of modal formulas of the form γ(x,p1,…,pn), where x occurs only positively in γ, we obtain the flat modal fixpoint language L♯(Γ) by adding to the language of polymodal logic a connective ♯γ for each γ∈Γ. The term ♯γ(φ1,…,φn) is meant to be interpreted as the least fixed point of the functional interpretation of the term γ(x,φ1,…,φn). We consider the following problem: given Γ, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L♯(Γ) on Kripke structures. We prove two results that solve this problem.First, let be the logic obtained from the basic polymodal by adding a Kozen–Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective ♯γ. Provided that each indexing formula γ satisfies a certain syntactic criterion, we prove this axiom system to be complete.Second, addressing the general case, we prove the soundness and completeness of an extension of . This extension is obtained via an effective procedure that, given an indexing formula γ as input, returns a finite set of axioms and derivation rules for ♯γ, of size bounded by the length of γ. Thus the axiom system is finite whenever Γ is finite.