Deprecated sections of set.mm

[Jon P]

Quick question: Why are the following sections marked as depricated in set.mm? 

PART 18  ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)

PART 19  COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

PART 20  COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)

Has anyone done other work on these areas which superceded them? Are there people working on these areas now or is there some plan to work on them? It seems like Hilbert Space stuff is quite an important topic to cover.

[Thierry Arnoux]

Yes, those have been superseded by the “extensible structure” definitions.

Section 10 covers the same material with extensible structures, and the new definition of Hilbert space is is 10.12.

Topological Groups, Rings, Fields and vector spaces are in section 12.2.

BR,

_

Thierry

Le 12 janv. 2020 à 02:33, Jon P <drjonp...@gmail.com> a écrit :



--
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/94154ce2-6f2a-42bf-8931-6626b4a614ae%40googlegroups.com.

[Alexander van der Vekens]

Hi Jon,

On Saturday, January 11, 2020 at 7:33:13 PM UTC+1, Jon P wrote:

Quick question: Why are the following sections marked as depricated in set.mm? 

PART 18  ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)

 

These areas are covered by  PART 10  BASIC ALGEBRAIC STRUCTURES

I am partially working in this area, proeparing some concepts of PART 18 like Magmas or Semigroups to be moved to PART 10 (see my mathbox). The definitions in PART 10 are, however, not based on the "standard" extensible structures, so these cannot be used without modification.

[Jon P]

Thanks both, I'll take a look :)

[Norman Megill]

On Saturday, January 11, 2020 at 1:33:13 PM UTC-5, Jon P wrote:

Quick question: Why are the following sections marked as depricated in set.mm? 

PART 18  ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)

PART 19  COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

The intent is for these deprecated sections to be deleted at some point in the future, once their theorems have extensible structure versions.  We could even start to prune them now:  we make a list of "terminal" theorems (i.e. theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it's not useful); if so, we delete it.  Then we repeat this recursively.  One way to search for terminal theorems, for example in deprecated group and ring theory, is to log the output ("open log x.txt") of "show usage cgr~circgrp" in metamath.exe and search for "(None)".
 

PART 20  COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)

The "Hilbert Space Explorer" section is deprecated because it starts from the axioms (not just definitions) for a single Hilbert space added to ZFC.  While this lets us have somewhat smaller proofs (since we don't have to say "Let H be a Hilbert space, let .+ be its vector addition operation,..." in every theorem), it is very restrictive and cannot for example express relationships between 2 Hilbert spaces.  Future theorems about Hilbert spaces should be done with extensible structures.

A lot of the theorems in the HSE have been "translated" to extensible structure versions, some of which are in my mathbox, but there is still a lot there that might be useful for future reference (such as operators, Riesz representation theorem, adjoints and bra-ket notation in infinite dimensions, an error bound for quantum computation, the lattice of closed subspaces).  It is much easier to translate these by hand from the HSE than to start from scratch from textbook proofs, since the HSE omits no details.

Norm

[David A. Wheeler]

Jon P wrote:
>> Quick question: Why are the following sections marked as depricated in
>> set.mm?

...

>> PART 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS
>(DEPRECATED)
>>
>> PART 19 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

Norman Megill:

>The intent is for these deprecated sections to be deleted at some point in

>the future, once their theorems have extensible structure versions...

>> PART 20 COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)

>The "Hilbert Space Explorer" section is deprecated because it starts
>from
>the axioms (not just definitions) for a single Hilbert space added to
>ZFC.

I intend to create a small pull request (a few lines in total) to document that information in those set.mm headers. That way future readers will know why it's there, and maybe even be encouraged to help.


--- David A.Wheeler

[Jon P]

So I tried a little with trying to find candidates for deletion from the deprecated sections by finding theorems which weren't referenced and then finding new theorems to pair them up with. I managed to do 9 here.

I am finding this task pretty hard, finding things in the database is not so easy. I might be able to write a python script to help with the searching, not sure.

[Norman Megill]

On Sunday, March 1, 2020 at 5:38:45 AM UTC-5, Jon P wrote:

So I tried a little with trying to find candidates for deletion from the deprecated sections by finding theorems which weren't referenced and then finding new theorems to pair them up with. I managed to do 9 here.

Thank you for starting this.
 

I am finding this task pretty hard, finding things in the database is not so easy. I might be able to write a python script to help with the searching, not sure.

What kinds of things you are having trouble locating?

Norm

[Jon P]

Glad to find something helpful :)

Re searching maybe an example would be helpful. So I was looking through the web page and scrolled up to ghomid and I wanted to find if the same concept is proven elsewhere. I guess I'd appreciate a tutorial for how others would go about that. 

The sort of things I do:

Open set.mm in a text editor and ctrl+f for specific phrases, like group homomorphism and then check the results.

Try to open what might be relevant pages on the website and scroll through them and read to see if there are any there, this can be time consuming. 

Search google in the hopes it will find the right page on the website. 

Things maybe I should try more of if they are better:

Using the MMJ2 search function.

Using metamath.exe search function.

I think the right partner for it is ghmid which I found by writing a python script which goes through set.mm and finds all theorems which contain "group", "homomorphism" and "identity" in their description.

I wrote a script which can compare the descriptions of two statements for general similarity however as you can see they are sufficiently differently worded to mean that technique didn't work so well.

In general any tips on searching would be really appreciated, thanks :)

[Mario Carneiro]

What I do:

* Search the metamath table of contents for group homomorphisms, or failing that, groups or something topical.

* Browse the section to see if it's there. Failing that:

* Identify the relevant constant (in this case, GrpHom)

* Use metamath's search tool to list all theorems containing this symbol, look for one that has the statement I'm looking for. You can search for a more precise string but this usually results in 50 or less results which is quick enough to exhaustively look over, and false negatives are unlikely at this point.

Mario

--

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/b6b20f0f-c642-4bb3-ac1d-04fa4f2fe6ed%40googlegroups.com.

[Norman Megill]

While my style is not the same as everyone's, it is rare that I go into set.mm in a text editor without knowing more or less what I plan to do (add a new theorem to prove, edit a comment, etc.).  I use the web pages to study proofs when I know the label but rarely search with e.g. google.  I use occasionally use grep on set.mm although sometimes it can be annoying because of all the graphics characters that need to be escaped.

For browsing, searching, getting information about usage, dependencies, etc. I spend much of my time in metamath.exe.  The main commands for that purpose are 'search', 'show usage', 'show trace_back', 'show statement', 'show proof'.  See 'help search', 'help show usage', etc. and study the help pages.  Most of them have qualifiers to help specify the output you want to see.  Here are some things I use frequently:

While not as rich as general regexes, labels can have wildcards * (match zero or more) and ? (match one), and multiple wildcard expressions can be separated by commas (no spaces) such as 'search *abc*,*def* ...'.  Math expressions in 'search' can have wildcards $* and $? (which can be abbreviated $ and ?, provided ? is not used in a math token).  The $? wildcard is peculiar; it means match one character in a token, not match one token; so "( ?? -> ?? )" will match "( ph -> ph )" but "( ? -> ? )" won't match anything.  Label ranges can be specified with <label>~<label>.

The '/comment' qualifier for 'search' means search comments.  '/join' means also search the $e hypotheses of a $p statement, joining them into a long string of tokens before the search:  "search * 'A = B $ |- $ C_'/join" will match sseq1i, sseq2i, sseq1d, etc.

'show usage' has a '/recursive' qualifier to show all direct and indirect uses of a statement.  'show trace_back ... /axioms /match ax-*' shows the axioms a proof depends on.  'show trace_back ... /to ...' will show just the path back to a specific statement, useful for e.g. debugging the unwanted usage of a certain axiom.

'show statement ... /comment' includes the comment above the statement.

Command keywords can be abbreviated e.g. 'sh tr' for 'show trace_back' as long as they are unambiguous.  This can save a lot of typing.  Single or double quotes are needed around multiple tokens, but if a quote ends the line you can omit the trailing quote character to save typing:  "search * '|- ph" will implicitly mean ""search * '|- ph'"

If you are using gcc to compile metamath, it's almost essential to call it via rlwrap so that you have command line editing, up-arrow command line history etc.  The pre-compiled metamath.exe for Windows has Windows-style command-line history built in.

I hope this helps a little.

Norm

[Jon P]

Thanks both for the help, that is very kind. 

One problem I came across while tracking down which theorems used the ones in 18.1.7 is I came across several in mathboxes. For example ghomf1o relies on ghomid which is in 18.1.7. 

My general question is how should theorems in mathboxes be handled if we are discussing removing 18.1.7? Do we need to replicate all theorems using the extensible structures in including all the ones in math boxes? What if they are odd theorems that other people aren't so interested in? Can we contact people and ask them to transfer them themselves? Is it ok to delete things from mathboxes without replacing them (I imagine this might be a problem for some people)? I feel this is a bit above my paygrade.

I think I might narrow my efforts down a bit just to doing theorem pairing (finding the new theorem which is the equivalent to the old). This is a task that needs to be done for all of parts 18, 19 and 20 and is non-controversial. I noticed some theorems, for example smgrpismgmOLD, have in their description a link to their new theorem. Is it ok if I start submitting pull requests which add links to theorems for which I have found pairs? Is it ok to add OLD to the name, presumably that is not allowed if there are any theorems that depend on it as it would break verification?

In that vein could I ask for some help with the following pairs? I think I have found the right thing but I am not sure. 

Is ghsubablo covered by ghmabl or is it to general?

Is ghsubgo covered by ghmima?

Is elghom paired with isghm? They use quite different symbols. 

For the rest I think I have all the pairs correct.

[Alexander van der Vekens]

Hi Jon

On Wednesday, March 4, 2020 at 11:46:58 AM UTC+1, Jon P wrote:

Thanks both for the help, that is very kind. 

One problem I came across while tracking down which theorems used the ones in 18.1.7 is I came across several in mathboxes. For example ghomf1o relies on ghomid which is in 18.1.7. 

Yes, I observed this already and asked how to handle these cases in a Github issue on 24-Jan-2020: https://github.com/metamath/set.mm/issues/1432#issuecomment-578288636

My general question is how should theorems in mathboxes be handled if we are discussing removing 18.1.7? Do we need to replicate all theorems using the extensible structures in including all the ones in math boxes?

No, nobody else should spent a lot of work for theorems in others' mathboxes (to shorten proofs or to replace names are exceptions, of course).

 

What if they are odd theorems that other people aren't so interested in?

Only the mathbox owner can/should judge if one of his/her theorems is odd.

Can we contact people and ask them to transfer them themselves?

Usually Norm does this, at least if no contact data is available.

Is it ok to delete things from mathboxes without replacing them (I imagine this might be a problem for some people)? I feel this is a bit above my paygrade.

Deletions should be done by the owner or by Norm (or on Norm's behalf).

I think I might narrow my efforts down a bit just to doing theorem pairing (finding the new theorem which is the equivalent to the old). This is a task that needs to be done for all of parts 18, 19 and 20 and is non-controversial. I noticed some theorems, for example smgrpismgmOLD, have in their description a link to their new theorem. Is it ok if I start submitting pull requests which add links to theorems for which I have found pairs? Is it ok to add OLD to the name, presumably that is not allowed if there are any theorems that depend on it as it would break verification?

Yes, this is a good idea, and I practiced it already (smgrpismgmOLD ). By this, the theorems are clearly marked as not to be used anymore, neither in new proofs nor in existing ones (i.e. have to be replaced sometime). By providing a date ("Obsolete version of ~ sgrpmgm as of 3-Feb-2020") everybody has enough time (usually about one year) to clean up his/her mathboxes until the lifetime of the OLD theorem expires and the OLD theorem (together with all theorems using it) is deleted.

In that vein could I ask for some help with the following pairs? I think I have found the right thing but I am not sure. 

Is ghsubablo covered by ghmabl or is it to general?

I think it is covered and can be deleted resp. tagged with OLD.

Is ghsubgo covered by ghmima?

 The same, it is covered and can be deleted resp. tagged with OLD.

Is elghom paired with isghm? They use quite different symbols. 

 The same, it is covered and can be deleted resp. tagged with OLD.  The symbols may be different, but the contents are qualitatively identical. By the way, the corresponding lemmata (elghomlem1 etc.) should also be suffixed by OLD and marked as "obsolete".

[Norman Megill]

I agree with Alexander's comments, and if you want to create a PR for this (renaming the to-be-deleted theorems as *OLD) it is fine.

It is preferable for the comment in *OLD to be e.g. "Obsolete version of ~ sgrpmgm as of 3-Mar-2020. " because when I look for expired theorems to delete, I would search for "Mar-2020. " in April 2021 (or if we wait until 2022, just "2020. ") where a space (or newline) follows the period.  Although the space after the period isn't mandatory nor an official convention, it can help speed up the cleanup process a little.

BTW a *OLD cleanup is a little overdue, and other people can do this as well, if anyone wants to volunteer.  All that is needed is simply to delete any *OLD theorem after a year from the "Obsolete..." comment; no entry in the list at the top of set.mm is needed.  But I would prefer that each case be inspected by hand before deletion to give it a final sanity check; an automated tool to do these deletions might be dangerous, for example if the date is suspicious, it might be a typo like typing 2019 instead of 2020.  Of course you should make sure that the *OLD isn't used ('verify proof * /syntax_only' would catch that instantly).  There are some *OLDs without an "Obsolete..." comment, which will require a judgment call; maybe it would be best to add an "Obsolete..." comment with today's date and otherwise leave it alone.  If the *OLD is in a mathbox, sometimes a little more care should be taken, since the mathbox user could just be experimenting with different versions of a theorem (but if it has an expired "Obsolete..." comment it should pretty much always be safe to delete).

Norm

[Norman Megill]

On Wednesday, March 4, 2020 at 5:46:58 AM UTC-5, Jon P wrote:

...

 

I think I might narrow my efforts down a bit just to doing theorem pairing (finding the new theorem which is the equivalent to the old). This is a task that needs to be done for all of parts 18, 19 and 20 and is non-controversial. I noticed some theorems, for example smgrpismgmOLD, have in their description a link to their new theorem. Is it ok if I start submitting pull requests which add links to theorems for which I have found pairs?

Yes.
 

Is it ok to add OLD to the name, presumably that is not allowed if there are any theorems that depend on it as it would break verification?

It won't break verification until the OLD is deleted.  However, if all theorems using it are also OLD (and with an earlier obsolescence date), it will be fine.  Indeed you may have to do that (i.e. rename theorems with usage to *OLD) once you start working back from endpoint theorems, since we don't actually delete them immediately but rename them to *OLD.

Norm