On Mon, 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). Then, > I would say that a scheme is an inference (resp. a deduction), if it is an > inference (resp. a deduction) associated with a (not necessarily true) > scheme. This brings us back to the original question. > > To summarize, let me denote a scheme by PHI => PSI where PHI actually > abbreviates PHI_1 & ... & PHI_n, with n=0 corresponding to "no > hypotheses". Also, I suppose that "phi" does not occur in those, and I do > not deal with DV conditions (we'll deal with ways to express non-freeness > later). 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 ) > > Note that yyyBi is roughly yyyi, so it is only a small abuse of language > to say that "yyyBi is the inference associated with yyy". > > Currently in set.mm, both the A and the B constructions are called > alternatively "the deduction associated with" and both use the label suffix > "d" (e.g. a1d versus mpd). As Mario mentioned, if n=0, then yyyiA == yyyB, > so they are closely related (and also xxxA == xxxk when n=0). But this is > not anymore the case when there are hypotheses. > 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. We can add another operation, the "closed form" operation, like so: >From the scheme xxx: PHI => PSI we derive xxxt: |- ( PHI -> PSI ) Then xxxt always has 0 hypotheses, and xxxti == xxx if PSI is not an implication. For a regular theorem xxx in inference form with all three variants, we have xxx == xxxti as the inference form, xxxt as the closed form, and xxxA as the deduction form. For a non-implication theorem with zero hypotheses, we have xxx == xxxt == xxxi as the closed form and xxxA as the deduction form. On Mon, Nov 29, 2021 at 10:30 AM David A. Wheeler <[email protected]> wrote: > Replying to myself - section 3.9.3 of the Metamath book defines > "closed form", "deduction form", and "inference form". See below. > > If we change deduction form to say "zero or more hypotheses" then > the categories are no longer exclusive. > 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. 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. > If we change the definition of "deduction form" so that it has zero or > more hypotheses, > then I think we ALSO need to change the definition of "closed form" > so it's "no hypotheses and its conclusion is NOT in the form ph -> ..." > (or some wording to that effect). That way, the categories are > mutually exclusive & cover all options. > 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. 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. 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.) > • closed form: A kind of assertion (theorem) with no hypotheses. > Typically its label has no special suffix. An example is unss, which > states: `((A ⊆C ∧B ⊆C) ↔(A ∪B) ⊆C) > • deduction form: A kind of assertion with one 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 or (2) a > definition. A definition can be for a class variable (this is a class > variable > followed by “=”) or a wff variable (this is a wff variable followed by > ↔); class variable definitions are more common. In practice, a proof > in deduction form will also contain many steps that are implications > where the antecedent is either that wff variable (normally φ) or is a > conjunction (...∧...) including that wff variable (φ). If an assertion is > in deduction form, and other forms are also available, then we suffix > its label with “d.” An example is unssd, which states12: `(φ →A ⊆ > C) & `(φ →B ⊆C) ⇒ `(φ →(A ∪B) ⊆C) > • inference form: A kind of assertion with one or more hypotheses > that is not in deduction form (e.g., there is no common antecedent). > If an assertion is in inference form, and other forms are also available, > then we suffix its label with “i.” An example is unssi, which states: > `A ⊆C & `B ⊆C ⇒ `(A ∪B) ⊆C > The only thing I would change here is "one or more" -> "zero or more", in both deduction form and inference form. This will make inference form and closed form overlap for theorems with no hypotheses/assumptions at all, and that's okay, it meets the criteria for both. -- 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/CAFXXJSuNOTkcQ3dZL_09DY1Ua5D7aDj3qffaSwL8-xK%2BouRZOA%40mail.gmail.com.
