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 -- 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 visit https://groups.google.com/d/msgid/metamath/13091f4d-0fa2-470d-836a-8b4d4108f889n%40googlegroups.com.
