On Monday, April 11, 2022 at 6:01:34 PM UTC+2 [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.
>
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?
--
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/7a0ab97a-d8f8-4fbd-bb06-88b16f63d714n%40googlegroups.com.
