> > 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). 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). 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. 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. Benoît -- 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/e27e8b51-85ae-4126-a385-06ef21e7870bn%40googlegroups.com.
