The "t" stands for "theorem", and it is used for theorem form when the "default" is not in theorem form for whatever reason. The "g" suffix (for "generalized" I think) is generally only used when the hypotheses being moved to antecedents are sethood hypotheses and the like.
On Mon, Apr 11, 2022 at 12:01 PM Jim Kingdon <[email protected]> wrote: > I suppose we should document "t" as meaning closed form (although it is > far less common than no suffix). We perhaps could get rid of "t" with a > modest amount of renaming (as far as I could tell from "show label *t"), > although when I look at something like all the *19.21* theorems, finding > good names for everything might be a touch complicated. > > On April 11, 2022 4:29:08 AM PDT, 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: >> >> There is a post of Norm ( >> https://groups.google.com/g/metamath/c/JWm26Y9qD-g/m/nhe6f87bBQAJ) withn >> the following statement: >> >> "Suffixes "i", "d", "t" mean inference, deduction, and closed theorem >> versions as usual." >> >> Unfortunately, there is no hint what "as usual" means/refers to. >> >> On Monday, April 11, 2022 at 1:17:27 PM UTC+2 Alexander van der Vekens >> wrote: >> >>> I noticed that there are many theorems with labels ending with "t", >>> having a statement like "Closed form of ..." in their comments. For example >>> ~trut: " A proposition is equivalent to it being implied by ` T. ` . >>> Closed form of ~ trud . ...". >>> >>> In the "conventions", it is written that theorems in closed form should >>> not have a special suffix, or should have suffix "g" in special cases. A >>> suffix "t" is not mentioned in the conventions. >>> >>> What does the "t" stand for? Should it be removed to follow the >>> conventions, or should the conventions be enhanced? In which cases a suffix >>> "t" should be used, and in which cases no special suffix? >>> >> -- > 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/6468E5E1-68E9-48CF-B220-81C16678CE8C%40panix.com > <https://groups.google.com/d/msgid/metamath/6468E5E1-68E9-48CF-B220-81C16678CE8C%40panix.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSu2Fu0-%2BTpduGLUubrPw7LadoXLe1njFc68z%3DxCwp8AzA%40mail.gmail.com.
