Metamath Proof Explorer


Theorem conventions-comments

Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding comments, and more generally nonmathematical conventions. For other conventions, see conventions and links therein.

(Contributed by the Metamath team">xxx, dd-Mmm-yyyy.)" (see Metamath Book, p. 142). The date cannot serve as a proof of anteriority since there is currently no formal guarantee that the date is correct (a claim of anterioty can be backed, for instance, by the uploading of a result to a public repository with verifiable date). The contributor is the first person who proved (or stated, in the case of a definition or axiom) the statement. The list of contributors appears at the beginning of set.mm.

An exception should be made if a theorem is essentially an extract or a variant of an already existing theorem, in which case the contributor should be that of the statement from which it is derived, with the modification signaled by a "(Revised by xxx, dd-Mmm-yyyy.)" tag.

  • Usage of parentheticals.

    Usually, the comment of a theorem should contain at most one of the "Revised by" and "Proof shortened by" parentheticals, see Metamath Book, pp. 142-143 (there must always be a "Contributed by" parenthetical for every theorem). Exceptions for "Proof shortened by" parentheticals are essential additional shortenings by a different person. If a proof is shortened by the same person, the date within the "Proof shortened by" parenthetical should be updated only. This also holds for "Revised by" parentheticals, except that also more than one of such parentheticals for the same person are acceptable (if there are good reasons for this). A revision tag is optionally preceded by a short description of the revision. Since this is somewhat subjective, judgment and intellectual honesty should be applied, with collegial settlement in case of dispute.

  • Explaining new labels.

    A comment should explain the first use of an abbreviation within a label. This is often in a definition (e.g., Definition df-an introduces the abbreviation "an" for conjunction ("and")), but not always (e.g., Theorem alim introduces the abbreviation "al" for the universal quantifier ("for all")). See conventions-labels for a table of abbreviations.

  • (Contributed by the Metamath team, 27-Dec-2016) Date of last revision. (Revised by the Metamath team, 22-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

    Ref Expression
    Hypothesis conventions-comments.1 𝜑
    Assertion conventions-comments 𝜑

    Proof

    Step Hyp Ref Expression
    1 conventions-comments.1 𝜑