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.
