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/54ca7750-1969-478a-bb18-121ff550e792n%40googlegroups.com. -- 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/2210502F-420F-4BDC-9107-F58FF3C0F4C8%40panix.com.
