Completeness for Flat Modal Fixpoint Logics

Abstract Given a set Γ of modal formulas of the form γ ( x, p ), where x occurs positively in γ, the language \(\mathcal{L}_\sharp({\it \Gamma})\) is obtained by adding to the language of polymodal logic K connectives \(\sharp_\gamma\), γε Γ. Each term \(\sharp_\gamma\) is meant to be interpreted as the parametrized least fixed point of the functional interpretation of the term γ ( x ). Given such a Γ, we construct an axiom system \({\bf K}_\sharp(\Gamma)\) which is sound and complete w. r. t. the concrete interpretation of the language \(\mathcal{L}_\sharp({\it \Gamma})\) on Kripke frames. If Γ is finite, then \({\bf K}_\sharp(\Gamma)\) is a finite set of axioms and inference rules.

Authors

• Luigi Santocanale
• Yde Venema

Keywords

No keywords are indexed for this paper.