×

General models and completeness of first-order modal \(\mu \)-calculus. (English) Zbl 1150.03008

The authors study the first-order modal \(\mu\)-calculus, i.e.the natural extension of the modal \(\mu\)-calculus with individual variables, flexible predicate symbols, and (first-order) quantifiers. They show in an accompanying technical report [K. Okamoto, A first-order extension of modal \(\mu\)-calculus. Programming Science Technical Report, PS-2006-003, Research Center for Verification and Semantics, National Institute of Advanced Industrial Science and Technology (2006)], using methods of I. Hodkinson, F. Wolter and M. Zakharyaschev [Ann.Pure Appl.Logic 106, No. 1–3, 85–134 (2000; Zbl 0999.03015)], that the set of valid formulas of the first-order \(\mu\)-calculus over standard Kripke models fails to be recursively enumerable and cannot be recursively axiomatised. This motivates the introduction of a broader semantics to ensure completeness. Correspondingly, a first-order extension of the notion of general frames, i.e.frames equipped with a set of distinguished propositions, is introduced, with respect to which the expected axiomatisation of the first-order \(\mu\)-calculus is proved complete. The associated model construction combines ideas from modal canonical model constructions and Henkin-style witnessed sets.

MSC:

03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science

Citations:

Zbl 0999.03015
PDFBibTeX XMLCite
Full Text: DOI