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. 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. --- David A. Wheeler ==== From section 3.9.3 ==== • 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 -- 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/D057F45C-88FE-49D0-978E-810A5C2D5D9D%40dwheeler.com.
