PS: In contrast to a label, the name/title needs not to be unique! It should only give a more descriptive hint to the meaning ot the theorem. For example, ~sbie, ~sbied and ~sbiedv could have the same title "Substitution conversion: implicit to explicit". That two of them are in deduction form or two of them use bound-variable hypotheses instead of distinct variable restrictions can/should be mentioned in the comment as usual (or this information can be obtained from the suffixes of the labels!).
On Saturday, January 4, 2020 at 9:12:55 AM UTC+1, Alexander van der Vekens wrote: > I fully agree with Norm that we should not change our general > conventions/usage of labels as "identifiers": they should be short, concise > and consistent (besides the primary property of being unique). Of course we > should still continue to improve the conventions and their usage. > > Since labels and comments seem to be not sufficient to understand theorems > and their proofs, the introduction of "names" or "titles" for theorems may > help. Actually, many comments consists of a name/title only (besides the > parentheticals), > e.g. ~necom: $( Commutation of inequality. (Contributed by NM, > 14-May-1999.) $), > > or the first sentence is like a name/title, > e.g. ~cramer: $( Cramer's rule. According to Wikipedia ... $). > > In many cases, however, the comment contains more information, and a > name/title cannot be "extracted" easily/automatically, > e.g. ~ixpn0: $( The infinite Cartesian product of a family ` B ( x ) ` > with an empty > member is empty. The converse of this theorem is equivalent to the > Axiom of Choice, see ~ ac9 . (Contributed by Mario Carneiro, > 22-Jun-2016.) $) > > I think the name/title of this theorem could be "Infinite Cartesian > product with empty member". To identify names/titles of theorems, we either > can use conventions (for example the first sentence of a comment, or the > part of the first sentence up to the first punctuation mark) or a special > parenthetical - for ~ixpn0 for example: > > $( (Title: Infinite Cartesian product with empty member) The infinite > Cartesian product of a family ` B ( x ) ` with an empty ... > > or an additional information comment - for ~ixpn0 for example: > > $( $j title Infinite Cartesian product with empty member $) > $( The infinite Cartesian product of a family ` B ( x ) ` with an empty ... > > Such a name/title could be used in the HTML/LATEX outputs, both in the > overview (new column "Title" or "Name" between columns "Label" and > "Description") and for a single theorem (in a new line "Title: ..." between > "Theorem <label>" and "Description: ....") and in the proofs (new column > "Title" or "Name" or "Theorem" between columns "Ref" and "Expression"). At > least such a name/title could be used as hover information (instead of > using the first part of the comment, which could contain more informatioin > than necessary/useful, e.g. for ~usgrass the hover text is "An edge is a > subset of vertices, analogous to ~ umgrass . (Contributed by Alexander..." > - "An edge is a subset of vertices" would be better/sufficient). > > What do you think about this approach? > -- 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/9760a350-09f7-4f91-9404-695c2bf3c303%40googlegroups.com.
