Suffix "t" for theorems in closed form.

[Alexander van der Vekens]

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?

[Alexander van der Vekens]

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.

[Jim Kingdon]

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.

[Mario Carneiro]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6468E5E1-68E9-48CF-B220-81C16678CE8C%40panix.com.

[Alexander van der Vekens]

On Monday, April 11, 2022 at 6:01:34 PM UTC+2 kin...@panix.com 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.

Yes, we either should document the meaning of suffix "t" in our conventions, or should eliminate it.

For the first option, I would suggest to enhance the item "Theorem forms." as follows:

      The labels of theorems in "closed form" would have no special suffix (e.g., ~ pm2.43 )

       or suffix "t" for "theorem" or "tautology" (e.g., ~ nfimt ).

       When an inference is converted to a theorem by eliminating an "is a set"
       hypothesis, we sometimes suffix the closed form with "g" (for "more
       general") as in ~ uniex vs. ~ uniexg .

This is justified already by the following subitem of item "Theorem forms." :

       <li>A theorem is in <b>"closed form"</b> if it has no $e hypotheses
       (e.g., ~ unss ).  The term "tautology" is also used, especially in
       propositional calculus.  This form was formerly called "theorem form"
       or "closed theorem form".</li>

For eliminating such suffixes "t", I had a look at  the first 277 occurences of suffix "t" in labels (there are currently 564 occurences in main set.mm). I found 38 cases in which the suffix "t" means "closed form" (either this is already indicated in the comment, or there is no other meaning of such a suffix, e.g., because it is part of another suffix like "const" for "constant") :

•     mtt*: closed form, but of what? ~mto? Then it should be called ~mtot (analogously to ~mtod). Without suffix "t", it can simply be called ~mt.
•     ancomst*: "Closed form of ~ ancoms ." - not really, it's a bijection => ~ ancomsb?
•     simplbi2comt: "Closed form of ~ simplbi2com" => ~simplbi2com -> ~simplbi2comi, ~simplbi2comt -> ~simplbi2com
•     trut: "Closed form of ~ trud." - not really, it's a bijection => ~ trub?
•     nftht: "Closed form of ~ nfth ." => ~nfth -> ~nfthi, ~nftht -> ~nfth
•     nfntht: "Closed form of ~ nfnth ." => ~nfnth -> ~nfnthi, ~nfntht -> ~nfnth
•     sylgt: "Closed form of ~ sylg ." => ~sylg -> ~sylgi, ~sylgt -> ~sylg
•     nfbiit*: "Closed form of ~ nfbii ." => ~nfbii -> ~nfbibii, ~nfbiit -> ~nfbibi
•     nfimt: "Closed form of ~ nfim" => ~nfim -> ~nfimi,  ~nfimt -> ~nfim
•     19.9t: "A closed version of ~ 19.9 ." => ~19.9 -> ~19.9i,  ~19.9t -> ~19.9
•     19.21t: "Closed form of Theorem 19.21 of [Margaris] p. 90, see ~ 19.21 ." => ~19.21 -> ~19.21i, ~19.21t -> ~19.21
•     19.23t: "Closed form of Theorem 1977.23 of [Margaris] p. 90.  See ~ 19.23 ." => ~19.23 -> ~19.23i, ~19.23t -> ~19.23
•     19.9ht: "A closed version of ~ 19.9h . " => ~19.9h -> ~19.9hi, ~19.9ht -> ~19.9h
•     hbnt: "Closed theorem version of bound-variable hypothesis builder ~ hbn ." => ~hbn -> ~hbni, ~hbnt -> ~hbn
•     spimt: "Closed theorem form of ~ spim . " => ~spim -> ~spimi, ~spimt -> ~spim
•     sbft: Closed form of ~ sbf => ~sbf -> ~sbfi, ~sbft -> ~sbf
•     nfsb4t: "(closed form of ~ nfsb4 )."   => ~nfsb4 -> ~nfsb4i, ~nfsb4t -> ~nfsb4
•     sbtrt: "Partially closed form of ~ sbtr ." => ~sbtr -> ~sbtri, ~sbtrt -> ~sbtr
•     r19.21t: "closed form of ~ r19.21 ." => ~r19.21 -> ~r19.21i, ~r19.21t -> ~r19.21
•     r19.23t: "closed form of ~ r19.23 ." => ~r19.23 -> ~r19.23i, ~r19.23t -> ~r19.23
•     ceqsalt: "Closed theorem version of ~ ceqsalg ." => ~ceqsalg -> ~ceqsalgi, ~ceqsalt -> ~ceqsalg
•     vtoclgft: "Closed theorem form of ~ vtoclgf ." => ~vtoclgf -> ~vtoclgfi, ~vtoclgft -> ~vtoclgf
•     vtoclegft: "(Closed theorem version of ~ vtoclef .)" => ~vtoclef -> ~vtoclefi, ~vtocleft -> ~vtoclef
•     spcimgft: "A closed version of ~ spcimgf ." => ~spcimgf -> ~spcimgfi, ~spcimgft -> ~spcimgf
•     spcgft: "A closed version of ~ spcgf " => ~spcgf -> ~spcgfi, ~spcgft -> ~spcgf
•     rspct: "A closed version of ~ rspc . " => ~rspc -> ~rspci, ~rspct -> ~rspc
•     elabgt: "(Closed theorem version of ~ elabg .) " => ~elabg -> ~elabgi, ~elabgt -> ~elabg
•     elrab3t: "(Closed theorem version of ~ elrab3 .)" => ~elrab3 -> ~elrab3i, ~elrab3t -> ~elrab3
•     sbciegft: "(Closed theorem version of ~ sbciegf .)" => ~sbciegf -> ~sbciegfi, ~sbciegft -> ~sbciegf
•     csbiebt: "(Closed theorem version of ~ csbiegf .)" => ~csbiegf -> ~csbiegfi, ~csbiebt -> ~csbiegf
•     csbie2t: "(closed form of ~ csbie2 )" => ~csbie2 -> ~csbie2i, ~csbie2t -> ~csbie2
•     copsex2t: "Closed theorem form of ~ copsex2g ." => ~copsex2
•     csbie2t: "(closed form of ~ csbie2 )" => ~csbie2 -> ~csbie2i, ~csbie2t -> ~csbie2
•     mosubopt: closed form of ~ mosubop => ~mosubop -> ~mosubopi, ~mosubopt -> ~mosubop
•     opelopabt: "Closed theorem form of ~ opelopab ." => ~opelopab -> ~opelopabi, ~opelopabt -> ~opelopab
•     fvmptt*: "Closed theorem form of ~ fvmpt ." => ~fvmpt => ~fvmpt2i, ~fvmptt => ~fvmpt2
•     nltpnft: closed form? => ~nltpnf
•     ngtmnft: closed form? => ~ngtmnf
•     shftidt: closed form? => ~shftid

My provided suggestions for renamings are straightforward (except for the labels marked with *, which may be discussed) and could be performed easily.

How should we proceed?

[Alexander van der Vekens]

Oh, I missed ~expt and ~impt, which are in closed form, but not (immediate) variants of ~ex and ~ imp. How should these be renamed?

[Mázsa Péter]

On Sun, May 8, 2022 at 3:02 PM 'Alexander van der Vekens' via Metamath
<meta...@googlegroups.com> wrote:
>
> (...) I would suggest to enhance the item "Theorem forms." as follows:
> (...)

> When an inference is converted to a theorem by eliminating an "is a set"
> hypothesis, we sometimes suffix the closed form with "g" (for "more
> general") as in ~ uniex vs. ~ uniexg .

We can eliminate hundreds of inferences with "is a set" hypothesis by
means of ~ elv , ~ el2v and ~ el3v , e.g. by deleting ~ uniex
(Contributed by NM, 11-Aug-1993.) and renaming ~ uniexg (Contributed
by NM, 25-Nov-1994.) to ~ uniex at the same time, and where you need
the inference form, use |- ( x e. _V -> U. x e. _V ) and ~ elv
(sometimes ~ ax-mp ). The main problem here is not mathematical: who
is the contributor of the remaining theorem? (Contributed by NM,
11-Aug-1993.) (Reviewed by NM, 25-Nov-1994.) ?

P.

[Alexander van der Vekens]

Hi Peter,
theorems in inference form are actually not "needed" at all, because they can always be replaced by using the closed form and applying ~ax-mp. Even theorems in closed form are not "needed", if a correspondig theorem is provided in deduction form, which is the preferred way to provide theorems. See the corresponding remarks in part "GUIDES AND MISCELLANEA".

I think there were a lot of discussions in the past if and how to keep theorems in inference form: either there are historical reasons, or many proofs can be shortend using them (saving the extra step ax-mp). With this post, it should be discussed if we really need two ways to express theorems in closed form (only to rename theorems: no theorems should be deleted, and no new theorems should be added).

Regarding your theorem ~elv: This can be applied only if sets (setvar variables) are involved. Are there really so many proofs which can be shortened using this theorem?
This could be checked by using the minimize script (checking all theorems using ~vex).

Alexander

[Alexander van der Vekens]

Regarding your theorem ~elv: This can be applied only if sets (setvar variables) are involved. Are there really so many proofs which can be shortened using this theorem?
This could be checked by using the minimize script (checking all theorems using ~vex).

Actually, there are already  115 proofs (of theorems up to ~fnse in alphabetical order - I had to stop the minimize script here because the checks of the fourier* proofs take too long...) which can be shortened already now (without any other modifications in set.mm). Therefore, it could be a good idea to move this theorem to main set.mm, immediately following ~vex. What do others think about this?

[Mázsa Péter]

On Mon, May 9, 2022 at 6:24 AM 'Alexander van der Vekens' via Metamath
<meta...@googlegroups.com> wrote:
> theorems in inference form are actually not "needed" at all, because they can always be replaced by using the closed form and applying ~ax-mp. Even theorems in closed form are not "needed", if a correspondig theorem is provided in deduction form, which is the preferred way to provide theorems. See the corresponding remarks in part "GUIDES AND MISCELLANEA".
> I think there were a lot of discussions in the past if and how to keep theorems in inference form: either there are historical reasons, or many proofs can be shortend using them (saving the extra step ax-mp).

Hi Alexander, you are right: I just wanted to avoid to populate my
Mathbox with inference forms and this is why I used only general forms
with ~ el*v* theorems instead. I'm not sure we should use them to
delete already existing inference forms. Perhaps this is a matter of
taste/tradition/heritage and does not need a general guideline.
Perhaps sometimes a purist will come up and eradicate "superfluous"
forms:) Thank you: Peter