On Tue, Nov 30, 2021 at 1:02 PM Benoit <[email protected]> wrote:
> Starting from a scheme >>> xxx: PHI => PSI >>> consider the two constructions: >>> xxxA: ( phi -> PHI ) => ( phi -> PSI ) >>> xxxk: PHI => ( phi -> PSI ) [examples: mp1i; bj-a1k; idd; etc. see >>> first two posts of this thread for several examples] >>> Starting from the scheme >>> yyy: PHI => ( PSI -> CHI ) >>> consider the two additional constructions: >>> yyyi: PHI & PSI => CHI [the inference associated with yyy] >>> yyyB: PHI & ( phi -> PSI ) => ( phi -> CHI ) >>> >> I would opt to call only the xxxA operation "deduction form". The yyyB >> operation is only putting the phi on some of the hypotheses, which is >> occasionally useful (and can be applied to an arbitrary subset of the >> hypotheses, so it's not a uniquely defined operation) but not very common. >> > > That's a detail, but yyyB is actually uniquely defined (look at the way > yyyB is obtained from yyy, not from yyyi, which was the line just above it, > which might explain the confusion). > Ah yes I see that, I mean to say that I would prefer to view it as an application of the partial-A operation on yyy': PHI & PSI => CHI (where by partial-A I mean that you only put "ph ->" on some subset of the hypotheses, in this case PSI). > > Anyway, your proposal makes sense: the "deduction associated with" refers > to the construction A, and also, by small abuse of language, to the > construction iA when n=0 (i.e. when yyy has no hypotheses). An example is > ax-1: ph -> (ps -> ph) which gives a1i: ph => ps -> ph, and then a1id: ch > -> ph => ch -> ( ps -> ph), but we label it a1d instead of a1id. > Collisions may appear when we want in set.mm the genuine A construction, > and not the iA construction (which is the B construction when n=0). This > is the case of bj-a1k, which is the genuine "deduction associated with > ax-1", while a1d is actually "the deduction associated with the inference > associated with ax-1". You seem to think that these cases are uncommon > enough to still use this abuse of notation and terminology. I do not have > a strong opinion either way, but one has to be aware of this small abuse of > notation and terminology (once settled, we'll edit the conventions > accordingly). > There is a reason that the case is uncommon, which is that it is explicitly discouraged to have theorems of the form ( A -> ( B -> C ) ) in deduction form (without good reason; as always, these are not hard and fast rules). For bj-a1k I'm fine with making an exception because it is (morally) in the propositional calculus section and there we allow anything at all, since you might need some crazy theorems during bootstrapping. But once things have settled down and you are doing a proof about locally compact manifolds or something you probably don't want to be using iterated implication. > We can add another operation, the "closed form" operation, like so: >> >> From the scheme >> xxx: PHI => PSI >> we derive >> xxxt: |- ( PHI -> PSI ) >> > > In my notation, PHI abbreviated PHI_1 & ... & PHI_n (but PSI and CHI are > single metaformulas), so to define xxxt, I guess that you mean either the > curried form (implication chain) or the uncurried form (one antecedent > which is a conjunction); this is up to permutation of the PHI_i's (and > association in the uncurried form), and suppose n>0, but these are minor > variants. > I mean the uncurried form, probably left associated too (although df-3an makes things complicated to specify here). In the case where n = 0, we define xxxt == xxx, i.e. no implication is introduced. > Then xxxt always has 0 hypotheses, and xxxti == xxx if PSI is not an >> implication. >> > > I do not understand why PSI being an implication makes a difference. > Maybe it's because by "xxxi", you mean the maximally iterated construction > xxxi....i ? Also, if there are n>1 hypotheses, things have to be stated a > bit more precisely, but I think the intention is clear. > I am being loose with currying. Assume every implication is uncurried. Then if xxx is A |- ( B -> C ) then xxxt is |- ( ( A /\ B ) -> C ) and xxxti is A, B |- C. On Tue, Nov 30, 2021 at 4:22 PM David A. Wheeler <[email protected]> wrote: > > 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. > The important part for naming is being able to recognize when a theorem is the deduction form counterpart of another theorem, or an inference form counterpart. For this purpose the rule is pretty clear: do lots of hypotheses and the conclusion have a wff metavariable assumption in them? Then it's deduction form. Have all the hypotheses been written as $e hyps instead of formulas before the ->? then it's inference form. Does it have a minimum of $e hypotheses and lots of hypotheses conjoined before the ->? Then it's in closed form. Is this exhaustive and handle all edge cases? Absolutely not, and that's okay. > 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. > I would say that it is an inference, but not that it is in inference form. Indeed, I rather like having 0-ary inferences still be technically inferences, because it unifies terminology, even if we would generally refer to those as axioms or closed statements instead. Metamath generally does not distinguish between having 0 or more $e hypotheses in its architecture, unlike traditional FOL that has "axioms" and "inference rules" and never shall they meet, which I think is silly because one is clearly a special case of the other. For "inference form" specifically, the idea is to support a proof strategy which is similar to deduction style but without the context, when you either don't need a context or can use dedth to simulate one. For example, ~strleun (like many automation lemmas) is in inference form, because the intent is to only ever have closed terms substituted for those variables, for which a context is not needed. If you put a "ph ->" on only the first hypothesis, then it would not compose properly - you can't pipe one strleun into another anymore, because it's not keeping the context empty. If the proof really required that, then it should switch to deduction form instead. Such a lemma I would call as neither inference form nor deduction form; it is violating the best practices of the form so it's nothing. It's an inference, but that's not much of a categorization because literally every $a/$t statement is an inference. > 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 mean the xxxA definition given in this thread. pntlema is not in the image of that operation. Of course it is in "deduction form" in the colloquial sense, but defining what this is precisely will result in a complicated definition with lots of exceptions which is not helpful to people, that's what I keep saying. 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. > We also need to include deductions that include |- G Struct < M , N > as a hypothesis, and lots of other things that are intended to be proved in the empty context. If you really want to catalogue this maybe you should put the information on the definition instead of in an already over-large "conventions" page. > > 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 don't mean to exclude these from "deduction form" at all. I mean to not define "deduction form" precisely, but only at the level of a dictionary or glossary definition. That is, be comfortable with an incomplete characterization, focus on the important features. My comparison to linguistics was deliberate: mathematics is a language, and sometimes defining what words mean is hard. Lots of things come with shades of detail, and if you rush to include them all then you will get something no human can understand anymore. > 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. > Or, put enough weasel words in the definition that it is clear that it is not a precise definition. 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. > Here are some relaxations that exist in the wild: * Some hypotheses don't have "ph ->": * A e. _V * N e. NN * A = ... * Some "A = ..." definitions *do* have "ph ->" * Some hypotheses are conjunctions like ph -> ( A /\ B ) (pntlema is like this) * The conclusion is ( ph /\ A /\ B ) -> C, i.e. some hypotheses are not written as $e hyps * Hypotheses might be written as "ph -> A. x e. A ps" or "( ph /\ x e. A ) -> ps" * There might be multiple wff metavariables, for example the conclusion is "( ph /\ ps ) -> B" and some of the hypotheses are "( ph /\ ps ) -> A" and others are "ph -> C" What I am proposing is to *ignore this* for the purpose of a glossary definition, and instead try to capture the salient features; mmnatded can talk about the reasons for using deduction form and the tradeoffs of these various relaxations. On Tue, Nov 30, 2021 at 4:41 PM David A. Wheeler <[email protected]> wrote: > > On Nov 29, 2021, at 3:43 PM, Benoit <[email protected]> wrote: > > As for the questions raised by David: in my opinion, the best term to > refer to hypotheses-free theorems is "hypotheses-free theorem", or "theorem > with no hypotheses" (in other words, no special term is needed; you can add > that it is also called a "closed form" theorem, and in a footnote, mention > that within propositional calculus, it is sometimes called a tautology or > simply a theorem, as opposed to an inference; however, it is more > convenient for us to use "theorem" also when there are hypotheses). > > It definitely gets confusing in some book sections & pages, e.g., > mmnatded.html and mmededuction.html. > > Currently they say: > > A deduction (also called an inference) is a kind of statement that needs > some hypotheses to be true in order for its conclusion to be true. A > theorem, on the other hand, has no hypotheses. (Informally we may call both > of them theorems, but on this page we will stick to the strict definition.) > An example of a deduction is the contraposition inference: > > It might be easier to say something like this: > > > Some theorems have one or more hypotheses; some have no hypotheses. > Within propositional calculus, the term "deduction" is sometimes used for > an assertion that has one or more hypotheses while "theorem" is only used > for assertions with have no hypotheses. In metamath terminology, all proven > assertions are termed theorems (whether they have hypotheses or not); to > clearly identify a subset you can refer to "theorems without hypotheses" or > "theorems with hypotheses" (the latter means "one or more hypotheses"). > In traditional parlance, a "theorem with hypotheses" would be called an "inference rule". Additionally, a "deduction" is synonymous for a proof. I don't think we need to define "deduction" at all, because our primary interest is in the "deduction theorem" and "deduction form", which are their own things. Reading the text as it is on the page, I don't think we need to make any changes. It seems good enough for pedagogy. We don't need to be talking about all the edge cases in the very first sentence following the header "introduction to deduction". Mario -- 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/CAFXXJSue9fJA0YF34mw%2BBVA2rb_zue-7LGcrcnV4_AoJauHDJg%40mail.gmail.com.
