Defining modal mu-calculus (or other fixed-point logics) in metamath?

[Xiaohong Chen]

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

[Jim Kingdon]

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.

[Xiaohong Chen]

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 to make it a congruence relation wrt all metalevel properties/tokens, and use it to introduce definitions (syntactic sugar). 

[Mario Carneiro]

Hi Xiaohong,

The wikipedia page on mu-calculus only contains syntax and semantics of the language, without any axiomatics. Presumably you would want to have some theorems about how the various symbols interact, because metamath isn't particularly interesting if there are no axioms to work with (unless you want to do this all "semantically" inside e.g. ZFC, in which case set.mm is as good as any place to work with it).

$c var act wff pos neg $. $( typecodes $)

$v X $. vX $f var X $.  $( variables $)

$v Y $. vY $f var Y $.

$v a $. aa $f act a $.  $( actions $)

$v ph $. wph $f wff ph $.  $( formulas $)

$v ps $. wps $f wff ps $.

$c ( ) [ ] -. mu $. $( symbols $)

wv $a wff X $.  $( a variable is a formula $)

wn $a wff -. ph $.  $( the negation of a formula is a formula $)

wa $a wff ( ph /\ ps ) $.  $( the conjunction of formulas is a formula $)

wbox $a wff [ a ] ph $. $( the box modality $)

${ wmu.1 $e pos X ph $. wmu $a wff mu X ph $. $} $( if X occurs positively in ph, then mu x ph is a formula $)

posv $a pos X X $. $( X occurs positively in itself $)

${ $d X ph $. posnf $a pos X ph $. $} $( if X doesn't appear at all in ph, then all occurrences are positive $)

${ $d X ph $. negnf $a neg X ph $. $} $( if X doesn't appear at all in ph, then all occurrences are negative $)

${ posn.1 $e neg X ph $. posn $a pos X -. ph $. $} $( if X appears negatively in ph, then it appears positively in -. ph $)

${ negn.1 $e pos X ph $. negn $a neg X -. ph $. $} $( if X appears positively in ph, then it appears negatively in -. ph $)

${ posa.1 $e pos X ph $. posa.1 $e pos X ps $. posa $a pos X ( ph /\ ps ) $. $} $( if X appears positively in ph, ps then it appears positively in ph /\ ps $)

${ nega.1 $e neg X ph $. nega.1 $e neg X ps $. nega $a neg X ( ph /\ ps ) $. $} $( if X appears negatively in ph, ps then it appears negatively in ph /\ ps $)

${ posbox.1 $e pos X ph $. posbox $a pos X [ a ] ph $. $} $( if X appears positively in ph, then it appears positively in [ a ] ph $)

${ negbox.1 $e neg X ph $. negbox $a neg X [ a ] ph $. $} $( if X appears negatively in ph, then it appears negatively in [ a ] ph $)

posmu1 $a pos X mu X ph $. $} $( X does not occur in mu X ph because it is bound $)

negmu1 $a neg X mu X ph $. $} $( X does not occur in mu X ph because it is bound $)

${ posmu.1 $e pos X ph $. posmu $a pos X mu Y ph $. $} $( if X appears positively in ph, then it appears positively in mu Y ph $)

${ negmu.1 $e neg X ph $. negmu $a neg X mu Y ph $. $} $( if X appears negatively in ph, then it appears negatively in mu Y ph $)

This covers the basic syntax, but it doesn't have any definitions in it, and it also has no axioms so there is little you can do beside prove that various expressions are well formed. This is also unusual as a metamath database, in that it uses variable typecodes that range over a non-context free grammar. One way to rectify this is to have no constraint in the wmu rule (construction of a mu expression), so that "ill formed" expressions make it into the type, but have provable judgments "|- pos X ph" and "|- neg X ph" that are required whenever you do anything nontrivial with a mu (like unfold it in its own definition).

$c |- = $. $( the meaning of "|- ph = ps" is that ph and ps are equivalent in all states. The "=" is just for show, it could also be just "|- ph ps" $)
${ posdef.1 $a pos X ps $. posdef.2 $a |- ph = ps $. poseq $a pos X ph $. $} $( unfold a definition in a "pos" proof $)
${ negdef.1 $a neg X ps $. negdef.2 $a |- ph = ps $. poseq $a neg X ph $. $} $( unfold a definition in a "neg" proof $)
eqid $a |- ph = ph $. $( reflexivity $)
$v ch $. wch $f wff ch $.
${ eqeuc.1 $e |- ph = ps $.
   eqeuc.2 $e |- ch = ps $.
   eqeuc $a |- ph = ch $. $} $( euclidean property (symmetry + transitivity) $)
${ neq.1 $e |- ph = ps $.
   neq $a |- -. ph = -. ps $. $} $( negation congruence $)
$v th $. wth $f wff th $.
${ aeq.1 $e |- ph = ch $.
   aeq.2 $e |- ps = th $.
   aeq $a |- ( ph /\ ps ) = ( ch /\ th ) $. $} $( conjunction congruence $)
${ boxeq.1 $e |- ph = ps $.
   boxeq $a |- [ a ] ph = [ a ] ps $. $} $( box congruence $)
${ mueq.1 $e |- ph = ps $. mueq.2 $e pos X ps $.
   mueq $a |- mu X ph = mu X ps $. $} $( mu congruence (need the side condition to ensure the mu's are well formed) $)

$c / nu $.
wsb $a wff [ X / ph ] ps $. $( substitution is a primitive constructor, with a recursive definition $)
sbv $a |- [ X / ph ] X = ph $. $( substitute an atomic variable $)
${ $d X ps $. sbnf $a |- [ X / ph ] ps = ps $. $} $( Substitution does nothing if X doesn't appear in ps $)
sbn $a |- [ X / ph ] -. ps = -. [ X / ph ] ps $. $( substitution into a negation $)
sba $a |- [ X / ph ] ( ps /\ ch ) = ( [ X / ph ] ps /\ [ X / ph ] ch ) $. $( substitution into a conjunction $)
sbbox $a |- [ X / ph ] [ a ] ps = [ a ] [ X / ph ] ps $. $( substitution into a box $)
${ $d Y ph $. nfpsb.1 $e pos Y ps $. nfpsb $a pos Y [ X / ph ] ps $. $}
  $( prove that a substitution has negative occurrences of Y when it doesn't occur in the substitution $)
${ $d Y ph $. nfnsb.1 $e neg Y ps $. nfnsb $a neg Y [ X / ph ] ps $. $}
  $( prove that a substitution has negative occurrences of Y when it doesn't occur in the substitution $)
${ ppsb.1 $e pos Y ph $. ppsb.2 $e pos X ps $. ppsb.3 $e pos Y ps $. ppsb $a pos Y [ X / ph ] ps $. $}
  $( prove that a substitution has positive occurrences of Y when it appears positively in the substitution $)
${ pnsb.1 $e neg Y ph $. pnsb.2 $e neg X ps $. pnsb.3 $e pos Y ps $. pnsb $a pos Y [ X / ph ] ps $. $}
  $( prove that a substitution has positive occurrences of Y when it appears negatively in the substitution $)
${ npsb.1 $e pos Y ph $. npsb.2 $e neg X ps $. npsb.3 $e neg Y ps $. npsb $a neg Y [ X / ph ] ps $. $}
  $( prove that a substitution has negative occurrences of Y when it appears positively in the substitution $)
${ nnsb.1 $e neg Y ph $. nnsb.2 $e pos X ps $. nnsb.3 $e neg Y ps $. nnsb $a neg Y [ X / ph ] ps $. $}
  $( prove that a substitution has negative occurrences of Y when it appears negatively in the substitution $)
${ sbmu1.1 $e pos X ps $.
   sbmu1 $a |- [ X / ph ] mu X ps = mu X ps $. $} $( substitution into a mu $)
${ sbmu.1 $e pos Y ps $. $d X Y $. $d Y ph $.
   sbmu $a |- [ X / ph ] mu Y ps = mu Y [ X / ph ] ps $. $} $( substitution into a mu (notice the side condition $d Y ph $.) $)

${ $d Y ps $. cbvsb $a |- [ Y / ph ] [ X / Y ] ps = [ X / ph ] ps $. $} $( alpha renaming in a substitution $)
${ cbvmu.1 $e pos X ps $.
   cbvmu $a |- mu Y [ X / Y ] ps = mu X ps $. $} $( alpha renaming in a mu $)

Now we have enough to actually write down the definitions, in a manner similar to the wikipedia page, and prove that the expressions involved are actually well formed:

$c -> <-> \/ < > $.
df-im $a |- ( ph -> ps ) = -. ( ph /\ -. ps ) $.
df-bi $a |- ( ph <-> ps ) = ( ( ph -> ps ) /\ ( ps -> ph ) ) $.
df-or $a |- ( ph \/ ps ) = ( -. ph -> ps ) $.
df-dia $a |- < a > ph = -. [ a ] -. ph $.
${ df-nu.1 $e pos X ph $.
   df-nu $a |- nu X ph = -. mu X -. [ X / -. X ] ph $. $}

We still don't have any axioms, and what's more, we don't even have a way to prove propositions. Here's a possibility:

${ ax-mpeq.1 $a |- ph = ps $. ax-mpeq.2 $a |- ph $. ax-mpeq $a |- ps $. $}
${ ax-l.1 $e |- ph $. ax-l $a |- ( ph /\ ps ) = ps $. $}
ax-id $a |- ( ph -> ph ) $.
ax-1 $a |- -. -. ph = ph $.
ax-2 $a |- ( ph /\ ps ) = ( ps /\ ph ) $.
ax-3 $a |- ( ( ph /\ ps ) /\ ch ) = ( ph /\ ( ps /\ ch ) ) $.
ax-4 $a |- ( ph -> ( ps /\ ch ) ) = ( ( ph -> ps ) /\ ( ph -> ch ) ) $.
ax-5 $a |- ( ph /\ ( ps -> ph ) ) = ph $.

${ ax-gen.1 $e |- ph $. ax-gen $a |- [ a ] ph $. $}
ax-mono $a |- ( [ a ] ( ph -> ps ) -> ( [ a ] ph -> [ a ] ps ) ) $.
${ ax-mucl.1 $e pos X ph $.
   ax-mucl $a |- ( [ X / mu X ph ] ph -> mu X ph ) $. $}
${ ax-muind.1 $e pos X ph $.
   ax-muind.2 $e ( [ X / ps ] ph -> ps ) $.
   ax-muind $a |- ( mu X ph -> ps ) $. $}

Anyway, this is a sketch of how you can define the rules of the mu calculus in metamath. Hopefully this will convince you that there is no practical limitation on what you can define using an appropriate choice of metamath axioms - as long as the definition is precise and reasonably algorithmic, you can construct an appropriate set of rules that mimic the desired behavior.

On Fri, Oct 18, 2019 at 11:32 AM Xiaohong Chen <cxiaoh...@gmail.com> wrote:

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 <cxiaoh...@gmail.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0c32789f-bec0-4208-9db5-c098fafb748e%40googlegroups.com.