> > On Mon, Nov 29, 2021 at 3:43 PM Benoit <[email protected]> wrote:
> On Mon, Nov 29, 2021 at 10:30 AM David A. Wheeler <[email protected]> > wrote: > If we change deduction form to say "zero or more hypotheses" then > the categories are no longer exclusive. > > On Nov 30, 2021, at 3:23 AM, Mario Carneiro <[email protected]> wrote: > I think this is not really the right way to look at it. They aren't > categories that are meant to be exclusive, they are operations that can be > applied to a theorem statement with various relations between them, like > Benoit has shown. However, it is convenient for discussion purposes to name a > statement after the operation that produced it, even if this isn't uniquely > defined in some cases. I *DID* intend for them to be exclusive; exclusive & complete categorizations are a lot easier to explain ;-). I'm okay with them being non-exclusive, but then we need to expressly say so. The purpose of these categories is to help people categorize & use assertions. More importantly, clear conventions make it easier for people to work together. > If you want a way to pick out deduction form theorems from others, the > obvious definition is the image of the deduction form operation (Benoit's > xxxA operation). Stated another way, a deduction form theorem is one such > that all (0 or more) hypotheses and the conclusion have the form "ph -> A" > for the same wff metavariable "ph". This overlaps with "closed form" if you > define it as a theorem with zero hypotheses, but I would say that anything in > the intersection should be considered in deduction form, not closed form, and > we can rationalize this by saying that a closed form theorem should not have > any wff metavariable assumptions. fvexd is not in closed form because it has > a useless metavariable hypothesis. An overlap is fine. We can say, "These are not exclusive, because some statements with no hypotheses can be simultaneously in closed form and deduction form. By convention we typically refer to these as being in deduction form (since they are, even if they aren't exclusively in this form)." > The categories are also not exhaustive. I would say that a theorem in > inference form should not have an implication as the conclusion, or else it > would not be in the image of the inference form operation (Benoit's yyyi > operation). But then A |- ( B -> C ) is neither closed form nor inference > form (and obviously not deduction form), and that's okay. Under our current definitions this is clearly inference form. E.g., mmnatded.html says: • Inference form: An assertion with hypotheses but no common antecedent is an "inference form"; it has a label suffix "i". We can change our definitions, obviously. Why is being in the image of this yyyi operation is so important? I'm honestly asking, I don't understand (maybe I'm missing the obvious). To me it's helpful saying "this is in inference form", and I believe the algorithm for converting deduction form to inference form works with *all* statements currently defined as being in inference form. I don't see the big advantage in losing the ability to explain that. > We're highlighting a particular structure of theorem that composes well, > exactly because not all theorems compose so nicely, and there are theorems > that don't fit any of the categories. (Plus, this is a very formalistic > categorization, and it doesn't fully explain all theorems you can find "in > the wild". For instance, ~pntlema is definitely written in "deduction style" > but it does not fit the rigid definition given here because some hypotheses > don't have a "ph ->" on them, and some hypotheses are conjunctions. Huh? pntlema *does* meet the definition of "deduction form" that we've been using for many years. The current definition of "deduction form" allows hypotheses to be either (1) (ph-> ...) or (2) definitions (using = or <->). pntlema meets the current definition of deduction form, and I think it should *continue* to be considered an example of deduction form. I also suggested expanding the definition of "deduction form" to allow a third case: not-free assertions without ( ph -> ...) statements. We have statements such as "alrimd" that are technically not in deduction form merely because they use F/, but are stated as being in deduction form. Let's expressly define them as being in deduction form. > It's certainly possible to extend the definition to accomodate this but at > some point it turns into formal descriptive linguistics and I don't think > that this is necessarily helpful for someone trying to learn the conventions.) Our *current* definitions allow for "definitions without a leading ph->", it's been that way for many years & it's clearly a useful construct. I think it *is* helpful to clearly define these conventions. Clearly defining them makes it much easier for everyone to follow them. If they're too restrictive, let's identify reasonable relaxations and include them in the definitions. I think that's particularly important for deduction form. How about this?" • deduction form: A kind of assertion with zero or more hypotheses where the conclusion is an implication with a wff variable as the antecedent (usually φ), and every hypothesis ($e statement) is either (1) an implication with the same antecedent as the conclusion, (2) a definition, or (3) a statement of not-freeness ` F/ ` . {... existing text ...} Are there any other relaxations for a theorem that would be sensibly called "deduction form"? The only one I can think of is where 1+ hypotheses are of the form: ( ( ph /\ ps ) -> ... ) Where "ph" is the common antecedent and ps are additions. I'm not really advocating for it, I'm simply pointing out that I think we add a few relaxations to the definition of "deduction form" so that others who want to use the form will easily know what they should be doing by convention. --- David A. Wheeler -- 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/2BA2088E-0F64-472B-ADB7-53C44B541C69%40dwheeler.com.
