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
--
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/681ab095-4446-48f1-ad4c-145a6e3a9eb5%40googlegroups.com.
