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. 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.
Benoît On Sunday, November 28, 2021 at 6:20:59 PM UTC+1 [email protected] 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 <[email protected]> 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/6e60c5a1-db5c-4858-a65d-1c4a20f5ade3n%40googlegroups.com.
