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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a5a858a1-3d70-4e40-996d-08fc31e7d061n%40googlegroups.com.
