Completeness for flat modal fixpoint logics

• Published in: Annals of pure and applied logic 2010-10, Vol.162 (1), p.55-82
• Main Authors: Santocanale, Luigi, Venema, Yde
• Format: Article
• Language: English
• Subjects: Axiomatization; Completeness; Computer Science; Fixpoint logic; Logic; Logic in Computer Science; Mathematics; Modal algebra; Modal logic; Representation theorem
• ISSN: 0168-0072
• DOI: 10.1016/j.apal.2010.07.003

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 , p 1 , … , p n ) , 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 K ♯ ( Γ ) 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 ♯ γ . 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 K ♯ + ( Γ ) of K ♯ ( Γ ) . 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 K ♯ + ( Γ ) is finite whenever Γ is finite.