- Completeness for flat modal fixpoint logics
- Annals of Pure and Applied Logic
- Volume | Issue number
- 162 | 1
- Pages (from-to)
- Document type
- Interfacultary Research Institutes
- Institute for Logic, Language and Computation (ILLC)
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 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 View the K♯+(Γ) is finite whenever Γ is finite.
- go to publisher's site
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.