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/07D81EFB-2AF4-4F14-8D6F-A38F05FE75D4%40dwheeler.com.
