Hi Peter, theorems in inference form are actually not "needed" at all, because they can always be replaced by using the closed form and applying ~ax-mp. Even theorems in closed form are not "needed", if a correspondig theorem is provided in deduction form, which is the preferred way to provide theorems. See the corresponding remarks in part "GUIDES AND MISCELLANEA".
I think there were a lot of discussions in the past if and how to keep theorems in inference form: either there are historical reasons, or many proofs can be shortend using them (saving the extra step ax-mp). With this post, it should be discussed if we really need two ways to express theorems in closed form (only to rename theorems: no theorems should be deleted, and no new theorems should be added). Regarding your theorem ~elv: This can be applied only if sets (setvar variables) are involved. Are there really so many proofs which can be shortened using this theorem? This could be checked by using the minimize script (checking all theorems using ~vex). Alexander On Sunday, May 8, 2022 at 6:21:53 PM UTC+2 Peter Mazsa wrote: > On Sun, May 8, 2022 at 3:02 PM 'Alexander van der Vekens' via Metamath > <[email protected]> wrote: > > > > (...) I would suggest to enhance the item "Theorem forms." as follows: > > (...) > > When an inference is converted to a theorem by eliminating an "is a set" > > hypothesis, we sometimes suffix the closed form with "g" (for "more > > general") as in ~ uniex vs. ~ uniexg . > > We can eliminate hundreds of inferences with "is a set" hypothesis by > means of ~ elv , ~ el2v and ~ el3v , e.g. by deleting ~ uniex > (Contributed by NM, 11-Aug-1993.) and renaming ~ uniexg (Contributed > by NM, 25-Nov-1994.) to ~ uniex at the same time, and where you need > the inference form, use |- ( x e. _V -> U. x e. _V ) and ~ elv > (sometimes ~ ax-mp ). The main problem here is not mathematical: who > is the contributor of the remaining theorem? (Contributed by NM, > 11-Aug-1993.) (Reviewed by NM, 25-Nov-1994.) ? > > P. > -- 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/15b3076a-0b3c-4434-a2ee-6b7a106ce587n%40googlegroups.com.
