Correction: the associated deduction is not what I wrote, but is as follows: if xxx : PHI_1 & ... & PHI_n => ( PHI -> PSI ) is a scheme, then the associated deduction is xxxd: PHI_1 & ... & PHI_n & ( phi -> PHI ) => ( phi -> PSI ) where phi does not occur in the PHI_i's or PHI or PSI.
Benoît On Sunday, November 28, 2021 at 12:31:39 PM UTC+1 Benoit wrote: > 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/3bd5452f-f5d6-4153-af92-b4b477b44956n%40googlegroups.com.
