General models and completeness of first-order modal mu-calculus
There is no recursive axiomatization of first-order modal mu-calculus that is complete with respect to usual Kripke models. Then we introduce general models, and we prove that the natural axiom system of first-order modal mu-calculus is complete with respect to general models.
general model completeness first-order modal mu-calculus kripke model modal logic