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 am not proposing a solution, here. Only summarizing the "problem". Maybe it's not even a big problem and people are content with it, but maybe also these varying conventions are a bit puzzling. I have no definitive opinion yet. Benoît On Monday, November 29, 2021 at 9:10:51 PM UTC+1 David A. Wheeler wrote: > If we're expanding the definition of "deduction form", can we also > allow hypotheses that directly state not-freeness in addition to ( ph -> > ...) and definitions? > It'd be one less thing to convert. If there's a reason NOT to do that, let > me know. > > If we do accept that, a first-cut detailed definition below (tweaking the > book's text). > > --- David A. Wheeler > > ===== > > > • 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 > (1) an implication with the same antecedent as the conclusion, or (2) a > definition, or (3) a direct statement of not-freeness. > 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 often 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) > • closed form: A kind of assertion (theorem) with no hypotheses > that is not in deduction form (e.g., it's not in the form ( φ → ...)). > Typically its label has no special suffix. An example is unss, which > states: `((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.” The deduction form is often the > inference > form with common antecedents added if both are present. > An example is unssi, which states: > `A ⊆C & `B ⊆C ⇒ `(A ∪B) ⊆C -- 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/0847d2f9-110a-46c8-bc0b-51c620bae49bn%40googlegroups.com.
