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. https://doi.org/10.1016/j.tcs.2011.11.026