Status of syl related renames

[jkingdon]

Sorry this is probably going to end up being long but in #4900 I said I'd try to summarize the whole situation.

In a nutshell we are talking about renames of names containing syl to names containing tr (syl5eqel to eqeltrid just to give one example of one that was renamed in 2023).

Let me describe some of the commonly discussed considerations:

1. The tr convention is widely used (for example in bitrd and eqtrd) and is naturally extended to im and im combined with bi.
2. At least as far as I've noticed, people have been happy with the renames which have been done so far (or maybe they've just been quiet).
3. The tr based names are in some cases longer than the syl based names. (counterpoint) we value shortness primarily as a way of reducing things like proof steps - reducing the number of bytes isn't the main point, at least these days
4. Since we are unlikely to have zero theorems using syl in the name (none of the proposals have gone that far), consistency calls for retaining syl itself and some core of names based on it
5. Most of these theorems are used a lot and people are used to the existing names
6. The word syllogism is widely used in the logic literature and (actually I won't try to summarize this family of arguments because they go in a few directions from here, ranging from discussion of how comments should be worded to the argument that syllogism is more appropriately applied to imim1 than the inference form syl, and maybe others).
7. Many tutorials and webpages mention syl so we'd want a discouraged theorem at that name if we did rename it (this seems to just apply to syl itself, not other names, as far as I have noticed)

Here I was thinking of adding an annotated and grouped list of possible future renames but at least for now I'll just copy-paste the relevant section of changes-set.txt as it exists now:

proposed  syl       imtri       (analogous to *bitr*, sstri, etc.)
                                there is less agreement on renaming syl
                                than others here
proposed  syld      imtrd
proposed  syldc     imtrdcom
proposed  syldd     imtrdd
proposed  sylbi     biimtri
proposed  sylib     imbitri
proposed  sylbb     bitriim
proposed  sylibr    imbitrri
proposed  sylbir    biimtrri
proposed  sylbbr    bitrriim
proposed  sylbb1    bitr3iim
proposed  sylbb2    bitr4iim
proposed  sylibd    imbitrd
proposed  sylbid    biimtrd
proposed  sylibrd   imbitrrd
proposed  sylbird   biimtrrd
proposed  syl5com   imtridcom
proposed  syl5      imtrid      alternate proposal: sylid
proposed  syl56     imtridi
proposed  syl5d     imtridd
proposed  syl5ibcom imbitridcom
proposed  syl5ibrcom imbitrridcom
proposed  syl6      imtrdi      alternate proposal: syldi
proposed  syl6com   imtrdicom
proposed  syl6d     imtrdid

Here are some of the past discussions:

• Expand proposed changes to *syl5* theorems #3556
• propose renames for some syl theorems #3569
• Pare back proposed renames for syl #4332
• Remaining proposed syl renames (group 2) #4504
• Remaining proposed syl renames (groups 3 and 4) #4505
• Rename syld to imtrd (iset.mm) #4900

[wlammen]

Many tutorials and webpages mention syl so we'd want a discouraged theorem at that name if we did rename it (this seems to just apply to syl itself, not other names, as far as I have noticed)

If necessary an alias (like id1) can keep references stable.