On Mon, May 9, 2022 at 6:24 AM 'Alexander van der Vekens' via Metamath <[email protected]> wrote: > 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).
Hi Alexander, you are right: I just wanted to avoid to populate my Mathbox with inference forms and this is why I used only general forms with ~ el*v* theorems instead. I'm not sure we should use them to delete already existing inference forms. Perhaps this is a matter of taste/tradition/heritage and does not need a general guideline. Perhaps sometimes a purist will come up and eradicate "superfluous" forms:) Thank you: Peter -- 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/CAJJTU5pUbFTAhH6gw4LQQyp4DF_%3D3Q%2BkGDNn-y1Li4i8aE_EAw%40mail.gmail.com.
