Dear Thierry,
I am thrilled seeing a Q0 implementation in the Metamath logical framework.
Some people at the HOL mailing list will be interested in this, too, so let me
copy to this list.
Unfortunately, I’m busy with my own projects and unable to get into
the details of Metamath currently, which seems very interesting.
However, it might help to have formalizations of the proofs at hand.
For example, Andrews’ theorems 5205, 5210, 5211, and 5212,
which you seem to have proven, are all formalized in the
R0 implementation:
http://doi.org/10.4444/100.10.3
To create an HTML file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.html
To create and automatically open the HTML file (Mac only), enter
make A5211.r0.out.html && open -a Finder $_
To create a PDF file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.pdf
To create and automatically open the PDF file (Mac only), enter
make A5211.r0.out.pdf && open -a Finder $_
PDF creation requires installation of LaTeX and pandoc.
More details can be found at
http://www.owlofminerva.net/files/README.txt
Best regards,
Ken Kubota
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
Link to mail and attachment:
https://groups.google.com/d/msg/metamath/I9obSTiuDl4/t-qoolnHAgAJ
> Am 18.05.2017 um 04:41 schrieb Thierry Arnoux <thierry.arn...@gmx.net>:
>
> Hi Mario, Norm, Cris, all,
>
> Curious about the Q0 language, and about whether Metamath can 'do Q0' just
> like it 'does set theory' in set.mm, I've started Q0 library in Methamath I
> wanted to share. I see this as a side project and don't plan to go very far,
> but wanted to share anyway.
>
> First, where would this go to? I would like to be able to share and track
> changes like we do with set.mm in GitHub. Shall I create a different
> repository or would this fit into any existing one?
> It's very small in size, so I'm attaching it to this mail to share a first
> version.
>
> Second, I have a technical question. While I can write all proofs using the
> metamath program, MMJ2 refuses to apply ~ mpeq and related theorems ( ~ mpbi
> , ~ r-f ). Is there anything I'm doing wrong? Or are there maybe special $j
> primitives that MMJ2 requires to apply those theorems? This is quite a
> handicap because ~ mpeq is probably going to be needed in nearly every proof.
> I wanted to ask you before I give up or dig into MMJ2 to understand $j ' use.
>
> I think I have a good starting point, but I see one caveat : the current ~ xa
> axiom states that variables can be of any type. I'm afraid this is maybe too
> flexible and could lead to contradictions, as one could use it twice in the
> same proof to give to one variable ` x ` two different types. This could
> actually not be a real issue, but anyway needs more thought.
>
> BR,
> _
> Thierry
>
>
> --
> 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+unsubscr...@googlegroups.com.
> To post to this group, send email to metam...@googlegroups.com.
> Visit this group at https://groups.google.com/group/metamath.
> For more options, visit https://groups.google.com/d/optout.
> <q0.mm>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
