Getting started with Metamath

[Mark Spindler]

I've become pretty intrigued by Metamath recently, and while the FAQ and various Youtube videos are helpful, I feel like I'm missing one or two pieces of information before I can really start to dig into it. The two main things I'm interested in are:

1. "Area of a Circle" still hasn't been proven in Metamath. Is there a thread (either in this Google Group or on some other site/medium) for a collaboration on this? Did someone start working on it get stuck? Is there a cold trail of "here's what we'd need to do first to approach it"? Since this has already been done in other systems, is there a big obstacle to translating this to Metamath?

2. I might be interested in toying with building up some new stuff (e.g. some combinatorial game theory). On the practical level, how do I use the Metamath program and/or mmj2 to create and manage a tower of new definitions and theorems? Is there an easy tutorial/other documentation explaining how to approach this sort of thing? Do I just add lines to the set.mm on my machine? Relatedly, what does it take to get a userbox and what is the use of one?

If these are covered well in some documentation/FAQ I missed, I'd be happy to know. Thanks for any direction you can provide.

[Mark Spindler]

Well, after a lot of work/exploring documentation, I think I'm a bit closer to having the answers to my questions, but I still am missing a lot of basic info.

• A lot of info on Metamath 100 progress seems to be at "Metamath 100... would love to see more" in the google group, and there are spin-off discussions on Github it seems.
  
• I haven't really figured out how to use mmj2 yet. For writing a proof I think I could figure it out by loading the various tutorial mmp files in turn, but I'm not sure how I'd use it for definitions and such.
• However, I found that I can add lines to the bottom of my local set.mm file and get them to work if I mimic metamath.pdf and/or David Wheeler's videos very carefully.
• Right now, my workflow for figuring out how to type things is 1. google "metamath [object]" to find a theorem/definition [whatever] about the object 2. Use metamath.exe with the commands "read set.mm" and "show statement [whatever]" and figure out that, say, (/) is the empty set. Is there an easier way to find the ASCII inputs on the metamath website directly?

As a test, I tried to make a function that gives the nth level of the hereditarily finite sets, and I think metamath.exe says they don't have syntax errors, but I'm not certain they say what they should/if I'm breaking some important/useful convention, etc.

$c heredfinf $.

cheredfinf $a class heredfinf $.

df-heredfinf $a |- heredfinf = ( n e. om |-> if ( n = 0 , (/) , ~P ( heredfinf ( n - 1 ) ) ) ) $.

Thanks for any help/direction!

-Mark

[Thierry Arnoux]

Hi Mark,

Overall I find the learning curve for Metamath quite steep, but David and others are really trying to make it more accessible. For example, I find the "Conventions" page recently added by David is a great resource. (http://us.metamath.org/mpeuni/conventions.html)

---

Globally, here is the way it goes for me - first on the method:

- I first do both the theoretical research about the theorems I'd like to prove, and search in Metamath set.mm already existing theories that are related, and already existing theorems that I could rely on. This includes the syntax of the already existing Metamath objects I'll use. This could go up to the level where, at least in my mind, I have a sketch of the proof and the main existing Metamath theorems I'll use.

- Then I start writing the new theorems I'd like to prove in an .mm file. I personally don't edit directly into set.mm but rather created myself a short file which first includes set.mm, and where I added my own theorems - this is just the same as adding at the end of set.mm, but keeps the file shorter and easier to manage.
Yours could look like that:

$[ set.mm $]

$c heredfinf $.

cheredfinf $a class heredfinf $.

df-heredfinf $a |- heredfinf = ( n e. NN |-> if ( n = 0 , (/) , ~P ( heredfinf ` ( n - 1 ) ) ) ) $.

$( There are countably many hereditarily finite sets. $)
heredfinfct $p |- heredfinf ~~ om $=
  ? $.

Note the theorem is written out, but I let the proof is kept open with a "?".
- Then, with MMJ2, I load the file several times and correct syntax errors until it accepts my file.
- Once my file can be opened in MMJ2, I start creating the proof using "New Proof".

Alternatively: I've been writing a plugin for Eclipse for Metamath, which really just encapsulates MMJ2, but which can be used to edit .MM files.
Here, the Metamath file is recompiled each time I save the file, and the error messages are updated in the "problems" window.
Once I want to move to the proof part, I then select the theorem name, right click and choose "Open in Proof Assistant" to start the proof part.


- For the proof itself, once you've opened the proof assistant: (I think this is well covered in David's video)
I'm taking my heredfinfct as an example here, I don't think it's too much of a spoiler but it can give an idea of the process.
For example, I found ~ fundmeng would be great to prove my theorem ~ heredfinfct. I then write a single line, before "qed", which looks like this:

100::fundmeng

And press "CTRL-U" to launch unification. This is then automatically completed as follows:

100::fundmeng      |- ( ( &C1 e. &C2 /\ Fun &C1 ) -> dom &C1 ~~ &C1 )

It is sufficient to replace one of the "&C1" instances and to press CTRL-U again to get it automatically filled in. This is very practical, as it avoids syntax errors:

100::fundmeng      |- ( ( heredfinf e. _V /\ Fun heredfinf ) -> dom heredfinf ~~ heredfinf )

Of course we shall use our definition ~df-heredfinf, too: this goes the same way.
I'm then obviously left with proving the following additional steps:

50:: |- heredfinf e. _V
90:: |- Fun heredfinf
150:: |- dom heredfinf ~~ om

Which I would prove using ~mptexg, ~funmpt, and ~dmmptg. : I go on filling in the blanks... For example, for step 90 here, ~funeqi is the last step I need.

---

Now on your definition:

I think what you've pasted below is still not syntactically correct. What you mean is probably something like:

df-heredfinf $a |- heredfinf = ( n e. NN |-> if ( n = 0 , (/) , ~P ( heredfinf ` ( n - 1 ) ) ) ) $.

I've replaced the om, which is the set of ordinal numbers, by NN, which is the set of integer numbers, on which ( n - 1 ) is defined. (You would probably use something like ` suc n ` in a definition using the ordinals, for the successor of a number). This is mentioned in David's Conventions.

I've also corrected the function value : ( heredfinf ` ( n - 1 ) ) is the way to compute the value of the function ` heredfinf ` at the point  ` ( n - 1 ) ` - note that here too, parenthesis are mandatory.

Finally, and this is probably the most important remark, which will make you write the definition completely differently, I suggest you follow David's advice on the conventions page about definition of recursive functions:

• Recursion. We define recursive functions using various "recursion constructors". These allow us to define, with compact direct definitions, functions that are usually defined in textbooks with indirect self-referencing recursive definitions. This produces compact definition and much simpler proofs, and greatly reduces the risk of creating unsound definitions. Examples of recursion constructors include recs(𝐹) in df-recs 6274, rec(𝐹, 𝐼) in df-rdg 6309, seq_𝜔(𝐹, 𝐼) in df-seqom 6346, and seq𝑀( + , 𝐹) in df-seq 10925. These have characteristic function 𝐹 and initial value 𝐼. (Σ_g in df-gsum 13279 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6274, but for the "average user" the most useful one is probably df-seq 10925- provided that a countable sequence is sufficient for the recursion.

I suggest you also study the already existing class of transitive sets, "Tr", which is related with your hereditarily finite sets, and "Fin", the class of finite sets.
Here you've got a choice to work at a higher level, with natural numbers and a definition using "seq", or at a lower level, where "Tr" is defined.

Regards,
_
Thierry

On 26/03/2017 06:56, Mark Spindler wrote:

Well, after a lot of work/exploring documentation, I think I'm a bit closer to having the answers to my questions, but I still am missing a lot of basic info.

• A lot of info on Metamath 100 progress seems to be at "Metamath 100... would love to see more" in the google group, and there are spin-off discussions on Github it seems.
  
• I haven't really figured out how to use mmj2 yet. For writing a proof I think I could figure it out by loading the various tutorial mmp files in turn, but I'm not sure how I'd use it for definitions and such.
• However, I found that I can add lines to the bottom of my local set.mm file and get them to work if I mimic metamath.pdf and/or David Wheeler's videos very carefully.
• Right now, my workflow for figuring out how to type things is 1. google "metamath [object]" to find a theorem/definition [whatever] about the object 2. Use metamath.exe with the commands "read set.mm" and "show statement [whatever]" and figure out that, say, (/) is the empty set. Is there an easier way to find the ASCII inputs on the metamath website directly?

As a test, I tried to make a function that gives the nth level of the hereditarily finite sets, and I think metamath.exe says they don't have syntax errors, but I'm not certain they say what they should/if I'm breaking some important/useful convention, etc.

$c heredfinf $.

cheredfinf $a class heredfinf $.

df-heredfinf $a |- heredfinf = ( n e. om |-> if ( n = 0 , (/) , ~P ( heredfinf n - 1 ) ) ) $.

[Mario Carneiro]

Sorry for not responding earlier, your message got lost in the shuffle.

On Wed, Mar 22, 2017 at 10:50 PM, Mark Spindler <mark.edwar...@gmail.com> wrote:

1. "Area of a Circle" still hasn't been proven in Metamath. Is there a thread (either in this Google Group or on some other site/medium) for a collaboration on this? Did someone start working on it get stuck? Is there a cold trail of "here's what we'd need to do first to approach it"? Since this has already been done in other systems, is there a big obstacle to translating this to Metamath?

Not much has been done in this direction. I tried to give a low-tech theorem statement at df-area and areacirc (commented out in set.mm), using iterated integrals in order to express area. That statement should be doable today, using trig substitution and so on, but it leaves much to be desired as far as the actual claim being made. What is really needed is a proper 2D Lebesgue measure, and measure theory appears to be moving forward thanks to Thierry's work, so we may not have to wait so long before this becomes possible.

 

2. I might be interested in toying with building up some new stuff (e.g. some combinatorial game theory). On the practical level, how do I use the Metamath program and/or mmj2 to create and manage a tower of new definitions and theorems? Is there an easy tutorial/other documentation explaining how to approach this sort of thing? Do I just add lines to the set.mm on my machine?

Currently, the best method, and the method I use, is just to write lines in set.mm. You craft the theorem statements using the same syntax as everything else, stub out the proofs with "?", then load it up in mmj2, whereupon it will error on all the stubbed proofs and you can get to work. When a theorem is completed in mmj2, you copy the proof body into set.mm and move on to the next. (There are some ideas for changing this workflow, but none are in production yet.)

 

Relatedly, what does it take to get a userbox and what is the use of one?

Just ask Norm, or add one yourself when you submit your first theorems. The purpose is to provide a "user space" for theorems that are (mostly) under your exclusive control, to test out ideas or works in progress. Once the work is sufficiently mature, it can go into the main library. We have a no-inter-mathbox referencing policy, so if you see a theorem in another mathbox you want to use, or I want to use your theorems, we can work to get it self contained and moved to main first.

On Sat, Mar 25, 2017 at 6:56 PM, Mark Spindler <mark.edwar...@gmail.com> wrote:

Well, after a lot of work/exploring documentation, I think I'm a bit closer to having the answers to my questions, but I still am missing a lot of basic info.

• A lot of info on Metamath 100 progress seems to be at "Metamath 100... would love to see more" in the google group, and there are spin-off discussions on Github it seems.
  

 There are also some remarks on a few of them in GitHub issues, and the mmrecent.html page mentions all the proven theorems as they come, but you've found most of what there is to find regarding metamath 100 theorems.

• I haven't really figured out how to use mmj2 yet. For writing a proof I think I could figure it out by loading the various tutorial mmp files in turn, but I'm not sure how I'd use it for definitions and such.

Yeah, as I mentioned I wouldn't use mmj2 for modifying set.mm, just for producing proofs of existing theorem statements.

• However, I found that I can add lines to the bottom of my local set.mm file and get them to work if I mimic metamath.pdf and/or David Wheeler's videos very carefully.
• Right now, my workflow for figuring out how to type things is 1. google "metamath [object]" to find a theorem/definition [whatever] about the object

I would suggest using either metamath SEARCH command to search statements and/or comments, or searching through set.mm with a text editor to find a definition by common name, label, or ascii symbol.

• 2. Use metamath.exe with the commands "read set.mm" and "show statement [whatever]" and figure out that, say, (/) is the empty set. Is there an easier way to find the ASCII inputs on the metamath website directly?

If you mouse over the GIF characters in the metamath website, it will show you the ascii symbol for it. Alternatively, you can search for the theorem in set.mm (i.e. just search for "0ex $p") or open the theorem in mmj2; in either case you will see the ascii, since of course these are all ascii display methods. Finally, there is the web page mmascii.html which will tell you the translation directly.

 

As a test, I tried to make a function that gives the nth level of the hereditarily finite sets, and I think metamath.exe says they don't have syntax errors, but I'm not certain they say what they should/if I'm breaking some important/useful convention, etc.

$c heredfinf $.

cheredfinf $a class heredfinf $.

df-heredfinf $a |- heredfinf = ( n e. om |-> if ( n = 0 , (/) , ~P ( heredfinf n - 1 ) ) ) $.

metamath.exe will have no problems with this because it does no grammar checking, but mmj2 should notice that df-heredfinf is not well-formed. Everything is fine except " ( heredfinf n - 1 )", which should be "( heredfinf ` ( n - 1 ) )" denoting function application. Once you've done that, mmj2 will find it grammatical, but if you run the definition checker, it will again complain, because it is a definition that refers to itself, so is not eliminable. We have a few direct methods for defining recursive functions. Also, om and NN0 are not the same set; 0 is an element of NN0, which is a subset of CC (complex numbers), while (/) is an element of om, which is a subset of On (ordinal numbers).

You probably want om here, since this is elementary set theory rather than number theory. You could achieve such a definition as:

df-heredfinf $a |- heredfinf = ( rec ( ( x e. _V |-> ~P x ) , (/) ) |` om ) $.

 

(It is worth mentioning that this already exists, in fact it is equal to "( R1 |` om )" (and you should view the R1 / rank theorems if you are interested in this). Or if you want the base set to be NN0 instead:

df-heredfinf $a |- heredfinf = seq 0 ( ( ( x e. _V |-> ~P x ) o. 1st ) , { <. 0 , (/) >. } ) $.

and theorem seq1st (and nearby theorems, and uses of this theorem) will help you prove the defining recursive equations for this definition.

On Sat, Mar 25, 2017 at 10:40 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Now on your definition:

I think what you've pasted below is still not syntactically correct. What you mean is probably something like:

df-heredfinf $a |- heredfinf = ( n e. NN |-> if ( n = 0 , (/) , ~P ( heredfinf ` ( n - 1 ) ) ) ) $.

I've replaced the om, which is the set of ordinal numbers, by NN, which is the set of integer numbers, on which ( n - 1 ) is defined. (You would probably use something like ` suc n ` in a definition using the ordinals, for the successor of a number). This is mentioned in David's Conventions.

Actually it should be NN0 for this definition, otherwise the "if n = 0" part is trivially not applicable.

 

I've also corrected the function value : ( heredfinf ` ( n - 1 ) ) is the way to compute the value of the function ` heredfinf ` at the point  ` ( n - 1 ) ` - note that here too, parenthesis are mandatory.

Finally, and this is probably the most important remark, which will make you write the definition completely differently, I suggest you follow David's advice on the conventions page about definition of recursive functions:

• Recursion. We define recursive functions using various "recursion constructors". These allow us to define, with compact direct definitions, functions that are usually defined in textbooks with indirect self-referencing recursive definitions. This produces compact definition and much simpler proofs, and greatly reduces the risk of creating unsound definitions. Examples of recursion constructors include recs(𝐹) in df-recs 6274, rec(𝐹, 𝐼) in df-rdg 6309, seq_𝜔(𝐹, 𝐼) in df-seqom 6346, and seq𝑀( + , 𝐹) in df-seq 10925. These have characteristic function 𝐹 and initial value 𝐼. (Σ_g in df-gsum 13279 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6274, but for the "average user" the most useful one is probably df-seq 10925- provided that a countable sequence is sufficient for the recursion.

I suggest you also study the already existing class of transitive sets, "Tr", which is related with your hereditarily finite sets, and "Fin", the class of finite sets.
Here you've got a choice to work at a higher level, with natural numbers and a definition using "seq", or at a lower level, where "Tr" is defined.

I will throw in the notations ( R1 ` om ) and U. ( R1 " om ) for hereditarily finite sets (if you search for these you will find a few theorems using them), as well as Hf in Scott Fenton's mathbox.

Mario