Many of your questions remind me of our questions about how to formalize CZF (in particular, the bounded formulas found in the separation axiom). The most well developed effort that I know of is at http://us2.metamath.org/ileuni/mmtheorems63.html#mm6265s
In the case of First Order Logic we had some work by Tarski to build from; for other logics it is a bit more a matter of covering new ground. For example, the current axioms for intuitionistic predicate logic - http://us2.metamath.org/ileuni/mmil.html#axioms - are generally based on the ones for classical predicate logic, but they diverge a bit more from any previous axiomization than, say, the axioms for IZF set theory or Intuitionistic propositional logic. Part of what you speak of also reminds me of our ongoing discussion of axioms versus definitions. In the metamath verifier itself, they are the same, but we have some conventions and tools which may or may not carry over easily into logics other than set.mm and iset.mm. On October 15, 2019 8:35:58 PM PDT, Xiaohong Chen <[email protected]> wrote: >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. -- 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/D37744E1-BAEE-4759-BC80-D5A8E1F61559%40panix.com.
