Late to the party, but I agree with Norm & Jim: Deductions can have 0 hypotheses, and while there is a naming conflict between whether the xxxd theorem is the result of "deductionizing" (add "ph ->" to all hyps and conclusion) the corresponding xxx or xxxi theorem, this is a rare situation. You could say that we have two operations: "make inference form" which converts |- ( A /\ B /\ C -> D ) to |- A & |- B & |- C => |- D, and "make deduction form" which adds "ph ->" to everything as mentioned. Usually when we have all three versions of a theorem, xxxi is the inference form of xxx, and xxxd is the deduction form of xxxi. In Benoit's example of bj-a1k, this is the deduction form of ax-1, skipping the a1i intermediary step.
The inference form operation is a no-op when the original theorem has no hypotheses, so you only have two forms for a theorem like fvex / fvexd. But the deduction form operation is not idempotent, you could always apply it multiple times and get everything under multiple layers of "ph -> ps -> ...", and we try to curry those iterated implications so that we can think of the deduction form operation as "effectively idempotent". Similarly, in the case where we have a theorem like ( A /\ B -> C ) we don't directly want to deductionize this because it yields an iterated implication |- ph -> ( A /\ B -> C ), and bj-a1k is an example of this. (There are some cases of deduction form theorems that retain some hypotheses in the conclusion; they are usually written as |- ( ( ph /\ A /\ B ) -> C ) though.) If you are hankering for a naming convention for deductionized "theorem form" theorems, I would suggest dusting off the *t naming convention for theorems as a base for the deduction suffix, to form "a1td". On Mon, Nov 29, 2021 at 12:07 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > I think Jim and Norm are right, so I will adapt the ~conventions > accordingly, and add a sentence about the special case "zero hypotheses". > > On Monday, November 29, 2021 at 4:59:50 AM UTC+1 Norman Megill wrote: > >> On Sunday, November 28, 2021 at 1:23:01 PM UTC-5 Benoit wrote: >> >>> Jim: indeed, maybe versions related to Mario's algorithm for the >>> deduction theorem should all be labeled xxxd, whether they have zero or >>> more hypotheses. >>> >> >> I agree with this, and I think we should change ~conventions to say >> "zero or more $e hypotheses" as Jim suggested. Using a 'd' suffix for a1i >> applied to a theorem has been a defacto convention for a long time and in >> many places, they are frequently used in Mario-style deductions, and I >> think people are used to it. >> >> >>> But the suffix "d" is still overloaded: in my previous post and its >>> correction, I gave two incompatible conventions of xxxd which are used in >>> set.mm (e.g., mpd for the first and a1d for the second). But then, >>> both a1d and bj-a1k could pretend to be "the deduction associated with >>> ax-1". Similarly for mpd versus mp1i with respect to ax-mp. Why in one >>> case choose one convention and in another the other convention ? For >>> clarity, the two versions of "associated deduction" could be better >>> distinguished, both by terminology and by systematic suffixing of a label. >>> >> >> I think this kind of conflict is very rare. The only one I could find >> with a quick search is a1d vs. bj-a1k. >> >> a1d follows the pattern of adding an antecedent to the hypothesis and >> conclusion of the corresponding a1i. The "a1" comes from the name of the >> inference form. A 0-hypothesis *d doesn't have a corresponding inference >> form, so we usually take the original theorem name and append a "d" suffix, >> e.g. fvex -> fvexd; following this pattern, bj-a1k would be named ax-1d, >> but since we reserve "ax-" for axioms, it could be called ax1d. >> >> I don't see a conflict with mpd vs. mp1i. The first hypothesis of mp1i >> doesn't have a "ph" antecendent, so it doesn't qualify as a "pure" >> deduction form. Maybe I'm misunderstanding what you mean. >> >> BTW many deductions such as alimd have the hypothesis "|- F/ x ph" where >> ph is the common antecedent, but this is equivalent to "|- ( ph -> F/ x ph >> )" by nf5di. So we could say it still qualifies as a "pure" deduction form >> where we use "|- F/ x ph" rather than "|- ( ph -> F/ x ph )" for brevity. >> >> Norm >> >> >>> >>> Benoît >>> >> >>> On Sunday, November 28, 2021 at 6:20:59 PM UTC+1 kin... @ panix.com >>> wrote: >>> >>>> Using "d" for these makes sense to me. >>>> >>>> If I want to try to be formal about it, I could say the below >>>> definition could read "zero or more $e hypotheses". But my reasoning is not >>>> primarily a formal one, it is more that using these feels like using a >>>> deduction theorem. They often satisfy hypotheses of other deduction >>>> theorems, they are parallel to non-deduction theorems (e.g. 1re vs 1red), >>>> when writing a proof I get to pick the antecedent, etc. >>>> >>>> Is there a particular problem we need to solve? Like do we have cases >>>> where the name we want is already taken? I do feel like adding finer and >>>> finer distinctions does add a level of cognitive burden so each one should >>>> pull its weight. >>>> >>>> >>>> On November 28, 2021 3:04:14 AM PST, 'Alexander van der Vekens' via >>>> Metamath wrote: >>>>> >>>>> By our conventions, >>>>> >>>>> >>>>> >>>>> >>>>> >>>>> *"A theorem is in "deduction form" (or is a "deduction") if it >>>>> has one or more $e hypotheses, and the hypotheses and the conclusion >>>>> are implications that share the same antecedent. More precisely, >>>>> the conclusion is an implication with a wff variable as the >>>>> antecedent (usually ` ph `), and every hypothesis ($e statement) is >>>>> either: ..."* >>>>> >>>>> There are, however, some theorems of the form `ph -> xxx ` which have >>>>> a label ending with "d", but are no "deductions" because they have no >>>>> hypotheses, e.g. >>>>> >>>>> ~eqidd, ~biidd, ~exmidd, ~fvexd >>>>> >>>>> These theorems are only convenience theorems saving an ~a1i in the >>>>> proofs(for example, ~eqidd is used 1441 times), but have no significant >>>>> meaning, because they always say "something true follows from anything". >>>>> >>>>> Is it justified that such theorems have suffix "d" although they are >>>>> no deductions? With a lot of good will, one can say that there is an >>>>> implicit hypothesis `ph -> T. ` (which is always true, see ~a1tru) which >>>>> would make these theorems deductions. Or would it be better to use a >>>>> different suffix or a complete different naming convention for such >>>>> theorems? >>>>> >>>>> -- > 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/3d3cf16d-3f83-453c-a5b1-9614e8093de6n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3d3cf16d-3f83-453c-a5b1-9614e8093de6n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs7sGiyDMjV4%3Dms-%3DDkCErrLPbHPtfeMEGqqCTzLz00_w%40mail.gmail.com.
