Rename 2p2e4 et al?

[icecream17]

conventions-labels states:

Focus on the important part of the conclusion. Typically the conclusion is the part the user is most interested in. So, a rough guideline is that a label typically provides a hint about only the conclusion; a label rarely says anything about the hypotheses or antecedents. If there are multiple theorems with the same conclusion but different hypotheses/antecedents, then the labels will need to differ; those label differences should emphasize what is different. There is no need to always fully describe the conclusion; just identify the important part. For example, cos0 15967 is the theorem that provides the value for the cosine of 0; we would need to look at the theorem itself to see what that value is. The label "cos0" is concise and we use it instead of "cos0eq1". There is no need to add the "eq1", because there will never be a case where we have to disambiguate between different values produced by the cosine of zero, and we generally prefer shorter labels if they are unambiguous.

(last sentence bolded)

Given this, should 2p2e4 et al be renamed 2p2? I think removing it does make the theorems a little bit easier to use; an exaggerated illustration of this is 235t711

Note that theorems like 1e0p1 would presumably be renamed to say, e0p1

Affected theorems

41306 0p1e1 $p |- ( 0 + 1 ) = 1
41308 1p0e1 $p |- ( 1 + 0 ) = 1
41309 1p1e2 $p |- ( 1 + 1 ) = 2
41319 2p2e4 $p |- ( 2 + 2 ) = 4
41329 2p1e3 $p |- ( 2 + 1 ) = 3
41330 1p2e3 $p |- ( 1 + 2 ) = 3
41331 1p2e3ALT $p |- ( 1 + 2 ) = 3
41332 3p1e4 $p |- ( 3 + 1 ) = 4
41333 4p1e5 $p |- ( 4 + 1 ) = 5
41334 5p1e6 $p |- ( 5 + 1 ) = 6
41335 6p1e7 $p |- ( 6 + 1 ) = 7
41336 7p1e8 $p |- ( 7 + 1 ) = 8
41337 8p1e9 $p |- ( 8 + 1 ) = 9
41338 3p2e5 $p |- ( 3 + 2 ) = 5
41339 3p3e6 $p |- ( 3 + 3 ) = 6
41340 4p2e6 $p |- ( 4 + 2 ) = 6
41341 4p3e7 $p |- ( 4 + 3 ) = 7
41342 4p4e8 $p |- ( 4 + 4 ) = 8
41343 5p2e7 $p |- ( 5 + 2 ) = 7
41344 5p3e8 $p |- ( 5 + 3 ) = 8
41345 5p4e9 $p |- ( 5 + 4 ) = 9
41346 6p2e8 $p |- ( 6 + 2 ) = 8
41347 6p3e9 $p |- ( 6 + 3 ) = 9
41348 7p2e9 $p |- ( 7 + 2 ) = 9
41987 9p1e10 $p |- ( 9 + 1 ) = ; 1 0
42360 5p5e10 $p |- ( 5 + 5 ) = ; 1 0
42361 6p4e10 $p |- ( 6 + 4 ) = ; 1 0
42362 6p5e11 $p |- ( 6 + 5 ) = ; 1 1
42363 6p6e12 $p |- ( 6 + 6 ) = ; 1 2
42364 7p3e10 $p |- ( 7 + 3 ) = ; 1 0
42365 7p4e11 $p |- ( 7 + 4 ) = ; 1 1
42366 7p5e12 $p |- ( 7 + 5 ) = ; 1 2
42367 7p6e13 $p |- ( 7 + 6 ) = ; 1 3
42368 7p7e14 $p |- ( 7 + 7 ) = ; 1 4
42369 8p2e10 $p |- ( 8 + 2 ) = ; 1 0
42370 8p3e11 $p |- ( 8 + 3 ) = ; 1 1
42371 8p4e12 $p |- ( 8 + 4 ) = ; 1 2
42372 8p5e13 $p |- ( 8 + 5 ) = ; 1 3
42373 8p6e14 $p |- ( 8 + 6 ) = ; 1 4
42374 8p7e15 $p |- ( 8 + 7 ) = ; 1 5
42375 8p8e16 $p |- ( 8 + 8 ) = ; 1 6
42376 9p2e11 $p |- ( 9 + 2 ) = ; 1 1
42377 9p3e12 $p |- ( 9 + 3 ) = ; 1 2
42378 9p4e13 $p |- ( 9 + 4 ) = ; 1 3
42379 9p5e14 $p |- ( 9 + 5 ) = ; 1 4
42380 9p6e15 $p |- ( 9 + 6 ) = ; 1 5
42381 9p7e16 $p |- ( 9 + 7 ) = ; 1 6
42382 9p8e17 $p |- ( 9 + 8 ) = ; 1 7
42383 9p9e18 $p |- ( 9 + 9 ) = ; 1 8
119809 1p1e2apr1 $p |- ( 1 + 1 ) = 2

41256 1m1e0 $p |- ( 1 - 1 ) = 0
41304 0m0e0 $p |- ( 0 - 0 ) = 0
41305 1m0e1 $p |- ( 1 - 0 ) = 1
41310 2m1e1 $p |- ( 2 - 1 ) = 1
41312 3m1e2 $p |- ( 3 - 1 ) = 2
41313 4m1e3 $p |- ( 4 - 1 ) = 3
41314 5m1e4 $p |- ( 5 - 1 ) = 4
41315 6m1e5 $p |- ( 6 - 1 ) = 5
41316 7m1e6 $p |- ( 7 - 1 ) = 6
41317 8m1e7 $p |- ( 8 - 1 ) = 7
41318 9m1e8 $p |- ( 9 - 1 ) = 8
225866 5m4e1 $p |- ( 5 - 4 ) = 1

41349 1t1e1 $p |- ( 1 x. 1 ) = 1
41350 2t1e2 $p |- ( 2 x. 1 ) = 2
41351 2t2e4 $p |- ( 2 x. 2 ) = 4
41352 3t1e3 $p |- ( 3 x. 1 ) = 3
41353 3t2e6 $p |- ( 3 x. 2 ) = 6
41354 3t3e9 $p |- ( 3 x. 3 ) = 9
41355 4t2e8 $p |- ( 4 x. 2 ) = 8
41356 2t0e0 $p |- ( 2 x. 0 ) = 0
42394 4t3e12 $p |- ( 4 x. 3 ) = ; 1 2
42395 4t4e16 $p |- ( 4 x. 4 ) = ; 1 6
42396 5t2e10 $p |- ( 5 x. 2 ) = ; 1 0
42397 5t3e15 $p |- ( 5 x. 3 ) = ; 1 5
42398 5t4e20 $p |- ( 5 x. 4 ) = ; 2 0
42399 5t5e25 $p |- ( 5 x. 5 ) = ; 2 5
42400 6t2e12 $p |- ( 6 x. 2 ) = ; 1 2
42401 6t3e18 $p |- ( 6 x. 3 ) = ; 1 8
42402 6t4e24 $p |- ( 6 x. 4 ) = ; 2 4
42403 6t5e30 $p |- ( 6 x. 5 ) = ; 3 0
42404 6t6e36 $p |- ( 6 x. 6 ) = ; 3 6
42405 7t2e14 $p |- ( 7 x. 2 ) = ; 1 4
42406 7t3e21 $p |- ( 7 x. 3 ) = ; 2 1
42407 7t4e28 $p |- ( 7 x. 4 ) = ; 2 8
42408 7t5e35 $p |- ( 7 x. 5 ) = ; 3 5
42409 7t6e42 $p |- ( 7 x. 6 ) = ; 4 2
42410 7t7e49 $p |- ( 7 x. 7 ) = ; 4 9
42411 8t2e16 $p |- ( 8 x. 2 ) = ; 1 6
42412 8t3e24 $p |- ( 8 x. 3 ) = ; 2 4
42413 8t4e32 $p |- ( 8 x. 4 ) = ; 3 2
42414 8t5e40 $p |- ( 8 x. 5 ) = ; 4 0
42415 8t6e48 $p |- ( 8 x. 6 ) = ; 4 8
42416 8t7e56 $p |- ( 8 x. 7 ) = ; 5 6
42417 8t8e64 $p |- ( 8 x. 8 ) = ; 6 4
42418 9t2e18 $p |- ( 9 x. 2 ) = ; 1 8
42419 9t3e27 $p |- ( 9 x. 3 ) = ; 2 7
42420 9t4e36 $p |- ( 9 x. 4 ) = ; 3 6
42421 9t5e45 $p |- ( 9 x. 5 ) = ; 4 5
42422 9t6e54 $p |- ( 9 x. 6 ) = ; 5 4
42423 9t7e63 $p |- ( 9 x. 7 ) = ; 6 3
42424 9t8e72 $p |- ( 9 x. 8 ) = ; 7 2
42425 9t9e81 $p |- ( 9 x. 9 ) = ; 8 1
183708 1t1e1ALT $p |- ( 1 x. 1 ) = 1

40411 1div1e1 $p |- ( 1 / 1 ) = 1
41328 2div2e1 $p |- ( 2 / 2 ) = 1
41357 4d2e2 $p |- ( 4 / 2 ) = 2

45814 4bc3eq4 $p |- ( 4 _C 3 ) = 4
45815 4bc2eq6 $p |- ( 4 _C 2 ) = 6
181454 5bc2eq10 $p |- ( 5 _C 2 ) = ; 1 0

55000 6gcd4e2 $p |- ( 6 gcd 4 ) = 2

55229 3lcm2e6woprm $p |- ( 3 lcm 2 ) = 6
55230 6lcm4e12 $p |- ( 6 lcm 4 ) = ; 1 2
55576 3lcm2e6 $p |- ( 3 lcm 2 ) = 6

184030 re0m0e0 $p |- ( 0 -R 0 ) = 0

41311 1e2m1 $p |- 1 = ( 2 - 1 )
42158 1e0p1 $p |- 1 = ( 0 + 1 )

(Not affected? and not already in the format:)

39428 00id $p |- ( 0 + 0 ) = 0
54902 gcd0val $p |- ( 0 gcd 0 ) = 0
119773 ex-bc $p |- ( 5 _C 3 ) = ; 1 0
119779 ex-lcm $p |- ( 6 lcm 9 ) = ; 1 8
184025 re1m1e0m0 $p |- ( 1 -R 1 ) = ( 0 -R 0 )
184029 sn-00id $p |- ( 0 + 0 ) = 0
219800 gbpart6 $p |- 6 = ( 3 + 3 )
219802 gbpart8 $p |- 8 = ( 3 + 5 )

[jkingdon]

I was wondering if 2p2e4 would better be 2add2, add22, or add2-2, in the sense that add is more common than p. I do see we list p in the table in https://us.metamath.org/mpeuni/conventions-labels.html with the text plus (see "add"), for all-constant theorems. Anyway, add versus p is perhaps a bit separate from the other issues here, so I won't discuss it further.

0p1e1 would be 0p1 . As for what to call 1e0p1 (which is just 0p1e1 with the equality commuted), I suppose the proposal of e0p1 establishes a convention of a leading e for commuted? 0p1com also springs to mind.

I could keep going on details, but I guess the more important question is whether the overall direction is a good one. I think so, at least in the sense that it better follows the convention, the convention seems to make sense (in general and as applied here), and I'm not thinking of cases in which including the "equals 4" in the name would ever disambiguate anything. I suppose there is the possibility that names as short as 1t1 might conflict with names using a totally different convention (existing or future) but even there I'm not necessarily thinking of why that would be especially likely.

[wlammen]

Also from the conventions page:
As a result, "two plus two equals four" is labeled [2p2e4](https://us.metamath.org/mpeuni/2p2e4.html)

So when introducing a new labelling scheme, you have to update the conventions page in this regard as well.

[digama0]

FWIW in MM0 I used names like d2mul4 for these lemmas, with the initial d indicating that this is using decimal numbers (the constant 0 is actually named d0, etc). I think for set.mm 2add2 would be sufficient. The p and e are only ever used in this specific set of theorems, so I think it could be ditched if we do this rename.

Note: Any changes to this set of theorems will also need to be reflected in the mmj2 macro which generates proofs of arithmetic statements. (Or maybe not? Seems the base case theorems are all picked up automatically in transformations.js. But if there are any other implementations of this algorithm floating around they may need updating.) Also, 2p2e4 is a theorem of historical interest which is linked in many places on the internet, so I would recommend making it an alias if it changes names.

[jkingdon]

Also, 2p2e4 is a theorem of historical interest which is linked in many places on the internet, so I would recommend making it an alias if it changes names.

I was wondering about this with respect to a different rename. What would "alias" mean? Have a theorem at the old name which is marked as discouraged, which has the same statement as the new name, and which I guess has a one step proof in terms of the new name?

If we want to reuse the name we do have precedent for that, the "Note on naming" at https://us.metamath.org/mpeuni/trud.html . But I don't know if there is an existing example of renaming a "well-known" theorem without reusing the old name.

[wlammen]

The idea of an alias is already present in set.mm. con4 is an alias for ax-3.

[icecream17]

It looks like "p" et al is used a bit more extensively than stated, like in cnambpcma --> cn ((a-b)+c)-a

It's going to be pretty hard to find all of these edge cases manually though. My affected theorem list searched for ( ? <symbol> ? ) = ? but that even misses o2p2e4

[digama0]

That looks like nonstandard naming, and it's in @avekens 's mathbox so we don't enforce the naming convention as strictly there. We don't use variable names in theorem names normally.

[icecream17]

I found another bunch of exceptions:

mulm1, adddirp1d

To avoid spamming the issue, I'll just edit this comment when I stumble on exceptions.

[avekens]

That looks like nonstandard naming, and it's in @avekens 's mathbox so we don't enforce the naming convention as strictly there. We don't use variable names in theorem names normally.

Yes, ~cnambpcma (and ~cnapbmcpd) were just experiments. They could be renamed as "subaddsubdif" and "addsubaddasscom" or something similar. I do not cling to these labels.

[avekens]

In my opinion, there is no need for any change: "p" and "m" are shorter than "add" and "sub", and the listed examples like 7m1e6 are intuitive and nice to read. Wheres "cos0" clearly means "cos(0)", it would not be so clear for "7m1". Therefore, the convention makes sense for "cos", but not for "m". And saving 2-3 characters is not worth the effort.