Sahlqvist theorem for modal fixed point logic

Citations of this article
Mendeley users who have this article in their library.


We define Sahlqvist fixed point formulas. By extending the technique of Sambin and Vaccaro we show that (1) for each Sahlqvist fixed point formula φ there exists an LFP-formula χ(φ), with no free first-order variable or predicate symbol, such that a descriptive μ-frame (an order-topological structure that admits topological interpretations of least fixed point operators as intersections of clopen pre-fixed points) validates φ iff χ(φ) is true in this structure, and (2) every modal fixed point logic axiomatized by a set Φ of Sahlqvist fixed point formulas is sound and complete with respect to the class of descriptive μ-frames satisfying χ(φ): φ∈Φ. We also give some concrete examples of Sahlqvist fixed point logics and classes of descriptive μ-frames for which these logics are sound and complete. © 2011 Elsevier B.V. All rights reserved.




Bezhanishvili, N., & Hodkinson, I. (2012). Sahlqvist theorem for modal fixed point logic. Theoretical Computer Science, 424, 1–19.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free