On Sunday, January 5, 2020 at 1:42:44 PM UTC-5, Alexander van der Vekens
wrote:
>
> Thanks, Norm, for these hints - it could have been expected that the
> discussion about labels is not new...
>
> Your approach, which I like very much, goes in a similar direction as my
> suggestion adding titels/names to the theorems, see
> https://groups.google.com/d/msg/metamath/XPYuatviNV0/C86R2MSqDQAJ. Of
> course, your approach is more systematic - having advantages (e.g.
> consistency,verifiability) and disadvantages (e.g. readability for humans,
> can become very long, especially if fully expanded - for example
> elfzom1p1elfzo
> -> "element_finite set of sequential integers_minus_1_plus_1_element_finite
> set of sequential integers) compared with my suggestion.
>
The problem is that this label "elfzom1p1elfzo" seems to be trying to fully
describe the theorem, which is a hopeless goal that causes more confusion
than it solves. I don't think anyone (except perhaps the author) could
figure out what the theorem states from this label (or even its expansion),
other than guessing it has something to do with half-open integer ranges
("fzo"). But its size makes it hard to remember and to type.
A label's purpose is to be a short identifier for a theorem. The
description provides more information, and finally the theorem itself
provides all of the information. All 3 of these can be searched to narrow
down candidate theorems to whatever degree of detail you want. The label
does not need to redundantly describe the theorem or its precise content.
All we need the label to do is to provide a hint about the nature of the
theorem and to be unique. The theorem is about membership of a successor
in a half-open integer range. The important pieces we need are "el"
(element), "p1" (successor), and "fzo" (half-open integer range). Unless
there are different variations that we need to distinguish, "p1elfzo" would
suffice. That's much easier to remember. Its expansion with an acronym
table would become "successor_element_halfOpenIntegerRange".
If there are two versions, say one for the more general "N e. ZZ" and this
one for "N e. NN", we can use "p1elfzo" for the general one and "p1elfzonn"
for this one specialized for NN. (I'm not sure why elfzom1p1elfzo is
specialized for NN, but I'm not familiar with its uses.)
Interestingly, "p1elfzo" is the last part of the original label, so the
original label partly had the right idea. It's just that it took it too
far and attempted to describe the entire theorem (unsuccessfully IMO).
Typically the conclusion is the part the user is most interested in. So a
possible rough guideline is to have the label provide a hint about the
conclusion and not (or rarely) say anything about the
hypotheses/antecedents.
We also don't need to fully describe the conclusion. For example, "cos0"
indicates the theorem provides the value for the cosine of 0, but we need
to look at the theorem itself to see what that value is. "cos0" is a good
label, whereas "cos0eq1" would not be.
Norm
--
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/74002793-8243-4e5e-b194-3181a515dc74%40googlegroups.com.
