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.
