Many thanks for this post. It will really help me a lot (and others too). :)
Olivier Le vendredi 1 novembre 2019 22:00:24 UTC+1, Norman Megill a écrit : > > (This continues the thread "question about fsumshft" > https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/t8WbKnW4DgAJ but is > more general, so I am starting a new thread.) > > A general issue raised by the previous thread is our convention for when > we should or shouldn't use "ph ->" as an antecedent for hypotheses in > theorems expressed in deduction form. > > There are four types of hypotheses (at least that I can think of right > now) where we usually do not use a "ph ->" antecedent in a theorem's > deduction form. Although it may weaken the theorem slightly, omitting this > antecedent where it is not needed can make proofs using the theorem > slightly shorter by not having to apply ~ a1i in order to match its > hypotheses. In the occasional situation where we need to strengthen the > deduction form with "ph ->" on one of these hypotheses, I indicate a > possible method. > > 1. Existence (sethood) hypothesis e.g.: > > $e ... |- A e. _V $. > > To add "ph ->", first turn the "A e. _V" into an antecedent using ~ vtoclg > and friends as in e.g. ~ unisng, then convert from this (semi-)closed form > back to deduction form. > > > 2. Not-free-in hypothesis e.g.: > > $e ... |- F/ x ps $. > $e ... |- F/_ x A $. > > I don't know of a good way to add "ph ->" in general. Worst case, the > theorem may have to be reproved back through a number of previous > theorems. We do have many "nf*d" theorems that will assist this. (If > anyone knows of a better method, let me know.) I think the need for "ph -> > F/ x ps" is pretty rare, though. > > The special case where ps is ph is given by ~ nfdi. > > > 3. Definitional hypothesis e.g.: > > $e ... |- ( ps <-> ( ch /\ th ) ) > $e ... |- A = ( B + C ) $. > > To add "ph ->", eliminate the original hypothesis with ~ biid or ~ eqid, > then rewrite the proof where the steps are simplified with the new "ph ->" > form of the definitional hypotheses. See also Mario's discussion at > https://groups.google.com/d/msg/metamath/V6QPBWzqvu4/jmY9kwLWCgAJ > > > 4. Implicit substitution hypothesis e.g.: > > $e ... |- ( x = y -> ( ph <-> ps ) ) $. > $e ... |- ( x = y -> A = B ) $. > > To add "ph ->", convert theorem to explicit substitution form, then > convert back to implicit substitution form. This can be somewhat tedious, > but at least it can be done in principle. See ~ fsumshftd for an example, > discussed at > https://groups.google.com/d/msg/metamath/vt6SqLrxEfo/tmogkcRPEgAJ > > -- 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/eb4afc4b-ccf9-4aa8-ad0a-11748a7b2e0b%40googlegroups.com.
