 Authors
 Year
 2010
 Title
 Completeness for flat modal fixpoint logics
 Journal
 Annals of Pure and Applied Logic
 Volume
 162
 Pages (fromto)
 5582
 ISSN
 01680072
 Issue number
 1
 Document type
 Article
 Faculty
 Interfacultary Research Institutes
 Institute
 Institute for Logic, Language and Computation (ILLC)
 Abstract

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 K♯(Γ) be the logic obtained from the basic polymodal K by adding a KozenPark 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 View the K♯+(Γ) is finite whenever Γ is finite.
 URL
 go to publisher's site
 Permalink
 http://hdl.handle.net/11245/1.334019
Disclaimer/Complaints regulations
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.