Thanks so much for the reference! I also found the definition of Peano arithmetics `peano.mm` that comes with the metamath distribution insightful. In general, the fact that `set.mm` can have a minimal definition of the metalevel of FOL is a bonus of FOL and not all logics can have that.
Now I feel free to define whatever infrastructures that are needed to implement the metalevel of my target logic. In particular, I defined a token `metaeq` denoting "metalevel equality", and define (metamath) axioms so that it becomes a congruence relation wrt all metalevel properties/tokens, and use it to introduce definitions (syntactic sugar). On Wednesday, 16 October 2019 10:57:25 UTC-5, Jim Kingdon wrote: > > 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] > <javascript:>> 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/0c32789f-bec0-4208-9db5-c098fafb748e%40googlegroups.com.
