(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/3923915f-00d3-4972-9ba6-16ece13a1cc4%40googlegroups.com.
