Thank you. I am thinking of using duplicating everything I write in text with the metamath language, but I think I'd prefer to build my own version of set.mm with my own proofs and also axiom and theorem names that match the text numbering and naming system. I can link to the equivalent result in set.mm for the important theorems. It would be nice to learn how to do this.
I also do not have a degree in logic and might need help with using proper terminology, but I will only be cover the deductive system (what's needed for metamath). This is a hobby. I have read some of the material and the site and have a few references of my own. The Stanford Encyclopedia of Philosophy has a good online introductory article called Classical Logic. On Tuesday, July 4, 2023 at 7:08:50 PM UTC-4 [email protected] wrote: > On 7/4/23 15:07, Marshall Stoner wrote: > > > What I'm writing is not directly connected with meta-math, but > > something that I feel could help explain it better for novices > > I'd advise you to follow where the inspiration leads you. If you end up > with something which has a lot of metamath notation and reference to > metamath theorems by name, that's great, and may indeed be helpful to > put on the web site in one form or another if you want to contribute it > in that fashion. If what you want to do (in terms of how it makes sense > to present the material or whatever) ends up diverging more from > metamath in detail and ends up being more of a general logic textbook, > that's cool too. > > > -- 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/12d384d3-364e-4423-aa09-2741be172190n%40googlegroups.com.
