That’s an excellent post regarding deductive logic and the complexity of getting started in meta math.
Meta math is in my opinion one of the pinnacles of modern mathematics. It is still a Wild West pioneering environment and there is plenty to do for everyone from newbies ( tell us how you got it working ) to experts. As more people get involved , the system will naturally self simplify as good documentation replaces worse. Don’t forget that we are dealing with pure mathematics here. It is art, not science! There are no wrong answers, only democratically approved better ones. If you have a scientific bent then please remember that truth is as subjectively true as objective truth. If you wish to preach from your wheelchair, then please don’t be offended if we don’t understand what you are saying! Finally, I will make the observation that women are not equal to men. This is easily demonstrated in all but a countable number of Von Neumann Univeraes! Monnington Sent from my iPhone > On 16 May 2024, at 9:06 PM, Jim Kingdon <[email protected]> wrote: > > On 5/16/24 04:02, 'ookami' via Metamath wrote: > >> I hope it is as simple as writing an E-mail to metamath at googlegroups.com. >> > As far as I know that works. > >> Converting a theorem into deduction form with 5 or more conjuncts will >> amortize after 1 or 2 usages. > > Once you get up to 5 or more conjuncts I don't think there is much > controversy on this point, and I don't think there would be much argument > about adding deductions (or replacing existing theorems with deductions) when > there are that many. > > Oh and in case anyone isn't familiar, the terms being discussed here are > described at "theorem forms" on > https://us.metamath.org/mpeuni/conventions.html > >> Here is one example https://us.metamath.org/mpeuni/add12.html 3 usages, 2 of >> which are proving inference and deduction version >> https://us.metamath.org/mpeuni/add12d.html 13 usages. >> > At least to my eyes this would seem like a case where we just need the > deduction form. Thanks for posting the counts on usages of each form. > >> I would also for consistency sake reformulate inference form theorems as >> deduction form. . . . And should you ever need the form without the >> antecedent you can easily use mptru. > > There might be a little less agreement about a statement which is this > global. The T. antecedents don't especially bother me but at least at some > times in the history of metamath having them around has not been loved. And > of course beyond a certain quantity of them, it might start running up > against some of our other desires, like shorter proofs. > >> The same I would also do for inference lemmas like 2+2=4 would become ph -> >> 2+2=4, so that future lemmas could directly use it if they ever need the >> fact that 2+2=4. > > We do this where the resulting deduction theorem would be frequently used, > like https://us.metamath.org/mpeuni/0red.html . As far as I've noticed in > cases like this (where the antecedent really is just to save an a1i, not > because there are any hypotheses) the deduction form would be in addition to > the closed form, not instead of. > > In a case of an equality, like this one, we have a bunch of theorems like > https://us.metamath.org/mpeuni/eqbrtrid.html which should help one to combine > deduction form with closed form. > >> Introduce new naming convention for those theorems in the section that would >> have no d suffix. Since there are only deduction form theorems it would not >> be necessary to suffix it anymore for a particular section. >> > That's going to be a bit section-by-section or theorem-by-theorem, but the d > suffix is used where it is needed to distinguish different theorems, not > globally for all deduction form theorems. > >> Also I had some issues with tooling, I couldn't get yamma to run and mmj2 >> was extremely hard to set up (issue with java version and deceiving runtime >> params), also mmj2 crashes and gives some unexpected NPE when I wanted to >> search something. I could help to improve the tooling, that is fine. > Pretty sure most of the tooling could use some love. Personally, I'm most > excited about the testsuites we have started to add to some of the tools, but > I suppose this isn't the place to go too deep into what would be the best > tooling-related things to work on. > > -- > 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/ab1bd88b-574f-41f1-8151-5fce550644b4%40panix.com. -- 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 visit https://groups.google.com/d/msgid/metamath/C64ACE1C-4CD2-40D2-BCD9-85B7C93EC219%40googlemail.com.
