Hi all, I recently got very interested in the metamath project and decided to use it to formalize other logics. I tried to define (the metalevel of) modal mu-calculus (https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus), which is a modal logic variant with direct support for least fixpoints and inductive reasoning.
However, I failed to get a minimal and simple definition of modal mu-calculus as that of FOL. I realized that for FOL, many of its metalevel properties such as free variables and proper substitution (for \forall-binder) can be "pushed down" to the object-level using some neat tricks (e.g., ax-5 for free variables, ax-12 for substitution) and thus are obtained "for free" by the FOL proof rules. For modal mu-calculus, however, those "neat tricks" no longer work. Modal mu-calculus has no \forall-binder. Instead, it has a \mu-binder that builds the least fixpoints, which obeys very different proof rules than FOL \forall-binder, so I don't know how to deal with free variables and proper substitution in modal mu-calculus without actually defining them in the metalevel. Also, modal mu-calculus has a more complex definition of its well-formed formulas. In its least fixpoint formula \mu X . phi, it requires that all free occurrences of X must not occur under an odd number of negations in phi. I don't know how to avoid explicitly defining these metalevel properties as we do in FOL. I can, of course, go and define all these metalevel properties (of modal mu-calculus) explicitly, but it leads to several annoying issues. Firstly, the definition is bigger and there are a lot more axioms to trust. Secondly, and more importantly, it makes defining derived constructs, or syntactic sugar constructs, or aliases, pretty tedious, because one needs to not only define the well-formed condition of the derived constructs but also all their metalevel properties (e.g., how to compute free variables for them? how to do proper substitution for them?). I tried to follow this approach for a while but gave up quickly because I found even I myself didn't trust the axioms I wrote. They were just too tedious and error-prone to write. I searched around the internet but couldn't find any metamath definitions of modal mu-calculus (or other fixed-point logics, which all have similar complex metalevels) that avoid explicitly defining its metalevel. Could anyone please give me some hints about the issue? Or kindly let me know if you are aware of any definition of modal mu-calculus in metamath. If needed I can elaborate on the difficulties using more concrete examples. Thank you in advance. Best wishes, Xiaohong -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2a33925d-f856-4c66-bcf5-2a11e0923462%40googlegroups.com.
