A modest proposal for the syl renames

[Matthew House]

Having used Metamath for a bit of time now, I have some thoughts on the syl-related renames. One thing that struck me about syl is that it is closely connected with mp. E.g., if you take an mp theorem with bare hypotheses, and add a common antecedent, you're likely to get a corresponding syl theorem:

ax-mp    -> syl
mp2      -> sylc
mp2b     -> 3syl
mpi      -> syl5com, mpan9, impel, syl5
mpisyl   -> syl2imc, syl2im
mpii     -> syl7
mpsyl    -> syl2im, syl2imc
mpbi     -> sylib
mpbir    -> sylibr
mpbii    -> syl5ibcom, imbitrid (= syl5ib)
mpbiri   -> syl5ibrcom, imbitrrid (= syl5ibr)
mpan     -> sylan
mpan2    -> sylan2
mp2an    -> syl2anc
mp4an    -> syl22anc
mpani    -> sylani
mpan2i   -> sylan2i
mpanl1   -> sylanl1 (also sylanl2, sylanr1, sylanr2)
mpbir2an -> sylanbrc
mpbir3an -> syl3anbrc
mp3an1   -> syl3an1 (also syl3an2, syl3an3)
mp3anl1  -> syl3anl1 (also syl3anl2, syl3anl3, syl3anr1, syl3anr2, syl3anr3)

And in the other direction, if you take a syl theorem and remove an antecedent from the conclusion, you're likely to get an mp theorem (if not another syl theorem):

syl        -> ax-mp
syld       -> syl, mpd
syldc      -> mpd, syl
syldd      -> syld, syld, mpdd
sylbi      -> ax-mp*
sylib      -> mpbi
sylbb      -> mpbi*
sylibr     -> mpbir
sylbir     -> ax-mp*
sylbbr     -> mpbir*
sylbb1     -> mpbi*
sylbb2     -> mpbir*
sylibd     -> sylib, mpbid
sylbid     -> sylbi, mpd*
sylibrd    -> sylibr, mpbird
sylbird    -> sylbir, mpd*
syl5com    -> mpi, syl
syl5       -> syl, mpi
syl6       -> syl, syl
syl56      -> 3syl
syl6com    -> syl, syl
syl5d      -> syl5, syld, mpid
syl6d      -> syl6, syld, syld
syl5ibcom  -> mpbii, sylib
syl5ibrcom -> mpbiri, sylibr
* antecedent removed from a biconditional in a hypothesis

This suggests that one possible characteristic for a syl theorem is "an mp theorem with additional antecedents and no bare hypotheses". In that sense, I would treat all syl theorems not involving biconditionals as relatively central to this idea, and it would be a shame if they were replaced with the proposed imtr* names. (There are some syl theorems derived from mpbi and mpbir, but preserving sylib/sylibr would introduce an asymmetry with sylbi/sylbir, so I don't feel so strongly about those names.)

If we do want naming consistency as our goal, I like the alternative options sylid/syldi for syl5/syl6. Indeed, we could extend the idea further, and use "partial deduction"-type names for many of the other syl theorems. The idea would be to start with ax-mp, mp2, and mp2b as our base theorems, and take syl (= mpdi), 3syl (= mp2bdii), and sylc (= mp2dd) as common abbreviations. (The syl*im* and syl*an* names can mostly be left alone, they're already pretty regular.) From here, we can name the rest of the implication-based syl theorems:

mpisyl    -> mp2di
sylcom    -> syldcom2 (syld with 2 commutations)
syl5com   -> sylidcom
syl11     -> comsylid (sylid preceded by a commutation)
syl5      -> sylid
syl6      -> syldi
syl56     -> 3sylidi
syl6com   -> syldicom
syli      -> syld3com
syl2im    -> syl2im
syl2imc   -> syl2imcom
syld      -> syld
syldc     -> syldcom
3syld     -> 3syld
sylsyld   -> mp2iddd
sylc      -> sylc
syl3c     -> syl3c    (by analogy with mpan/mp3an)
syl6mpi   -> mp2di2
mpsyl     -> mp2id
mpsylsyld -> mp2id2
syl6c     -> sylcdd
syl6ci    -> sylcdidd
syldd     -> syld2
syl5d     -> sylidd
syl7      -> sylid2
syl6d     -> syldid
syl8      -> syldi2
syl9      -> syliddi
syl9r     -> syldiid
syl10     -> mp2iddd2

Of course, it wouldn't have to be exactly like this, I'm just bringing it up as a more complete alternative to the imtr* idea. The overall intent would be to introduce consistency without leaving the syl*im* and syl*an* names unmoored, nor breaking the connection between syl and mp theorems.

Matthew House