document why some sections are deprecated

[david-a-wheeler]

Document why certain sections are deprecated, as described in this set of email messages.

On Saturday, January 11, 2020 at 1:33:13 PM UTC-5, Jon P wrote: Quick question: Why are the following sections marked as deprecated 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 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

[nmegill]

I corrected a mistake I made (edited your comment directly): I changed "deprecated group and ring theory" to "deprecated group theory".

[david-a-wheeler]

This is done. Thanks!