Most theorems which involve applying transitivity are named according to
a pattern
XXYYtr
where XX and YY are abbreviations for what kind of theorem this is and
then the usual suffixes apply. Examples:
eqeltrd
sseqtri
And if XX and YY are the same the abbreviation is only listed once, for
example:
sstri
bitrd
.... and many others.
One notable family of theorems that do not use this convention are the
various theorems named with syl (syl, syl5, syl6, sylbi, etc). Many
years ago, Norm proposed that we should use the "tr" convention for
these too. To quote directly (in text now in changes-set.txt):
This is part of an ongoing project to improve naming consistency. . . .
PROPOSED:
Date Old New Notes
proposed syl imtri (analogous to *bitr*, sstri, etc.)
proposed sylib imbitri etc.
proposed sylbid biimtrd etc.
proposed sylbird biimtrrd etc.
proposed syl5* *trid (syl5bi -> biimtrid; syl5eqel ->
eqeltrid;etc.)
proposed syl6* *trdi
This is obviously a big change in the sense that the theorems to be
renamed are some of the most commonly used theorems in set.mm. But the
more I have been thinking about this the more I like the idea and am
pretty sure that once I got used to it the new names would be quite
natural and fit nicely with the many theorems which already use the "tr"
convention.
There's an issue here: https://github.com/metamath/set.mm/pull/3556
which proposes new names for individual theorems, starting with the
current *syl5* theorems. But it hasn't gotten enough discussion
(positive, negative, or otherwise) to either go ahead, formulate an
alternative proposal, decide we like the status quo, or whatever. Even
go ahead I suppose has multiple sub-options: to go ahead fairly quickly
(as we did with the mpt2 -> mpo renames) or go ahead more slowly (maybe
state a plan to do it over time, or whatever form that would take).
--
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/fed489b3-9325-4e7f-950b-2850b0ea91c2%40panix.com.
