I had noticed this too, and was thinking of the suffix "k" (for "weaKening" and because ax-1 is often called "axiom K").
It currently has the suffix "d" because it works together with the genuine deductions to implement Mario Carneiro's algorithm related to the deduction theorem (his slides are on the metamath website). But I think having another suffix makes things clearer (beginning with ~idk). In other words, you have the two notions of "associated deduction" and "associated weakening": if xxx : PHI_1 & ... & PHI_n => PHI is a scheme (with n=0 corresponding to "no hypotheses"), then the associated deduction is xxxd: ( phi -> PHI_1 ) & ... & ( phi -> PHI_n ) => ( phi -> PHI ) and the associated weakening is xxxk: PHI_1 & ... & PHI_n => ( phi -> PHI ) In predicate calculus, there may be minor variations to deal with uses of ax-gen (using either DV conditions or non-freeness or related idioms), and variations concerning "definitional hypotheses" which may lack the antecedent. Benoît On Sunday, November 28, 2021 at 12:04:14 PM UTC+1 Alexander van der Vekens 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/29c96d89-a417-4321-a757-97f2d98159d7n%40googlegroups.com.
