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 Gamma of modal formulas of the form gamma(chi, p(1), ..., p(n)), where chi occurs only positively in gamma, we obtain the flat modal fixpoint language L-#(Gamma) by adding to the language of polymodal logic a connective #(gamma) for each gamma is an element of Gamma. The term #(gamma) (phi(1), ..., phi(n)) is meant to be interpreted as the least fixed point of the functional interpretation of the term gamma(chi, phi(1), ..., phi(n)). We consider the following problem: given Gamma, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L-#(Gamma) on Kripke structures. We prove two results that solve this problem. First, let K-#(Gamma) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective #(gamma). Provided that each indexing formula gamma 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 K-#(+) (Gamma) of K-#(Gamma). This extension is obtained via an effective procedure that, given an indexing formula gamma as input, returns a finite set of axioms and derivation rules for #(gamma), of size bounded by the length of gamma. Thus the axiom system K-#(+) (Gamma) is finite whenever Gamma is finite. (C) 2010 Elsevier B.V. All rights reserved.