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 <[email protected]>
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 <[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/0c32789f-bec0-4208-9db5-c098fafb748e%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/0c32789f-bec0-4208-9db5-c098fafb748e%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAFXXJSssw29-%2BpMb9B6%3DVGFao2H142RpekND9Y_XBh87BPQZdA%40mail.gmail.com.
