Well! I am finally starting to really "dig" Ghilbert. I like many things about it very much. So I am considering stealing as much as possible from Ghilbert which is 100% consistent with direct convertability between it and Metamath. This means another flavor of Ghilbert, which I would tenatively name "mmjbert" because the dialect would provide services to the totally hypothetical vaporware product, "mmj3" (which we would like to be able to handle multi-core, multi-computer parallel/distributed processing environments.)
Here are the main concept variations from Ghilbert Prime:
Definitions of the Ghilbert variety revert to being just Axioms, as they are in Metamath. I believe I see what the intent is for Ghilbert definitions and it is admirable but de-selected for mmjbert. Here is why.
Look at the "definition" for df-3or. This is an equivalency back to "2or" -->
( ph \/ ps \/ ch \/ ) <-> ( ( ph \/ ps ) \/ ch )
Which is fine, of course. But according to the Ghilbert specification, during proof verification when a definition is encountered during the matching process, and it doesn't match its corresponding node, the definition is expanded, which is totally logical of course. But it is treating df-3or as syntactic sugar. And that is "ok" too, except that it will not fly in Metamath, which is what mmjbert must service.
Metamath has a number of "syntactic sugar" syntax axioms. In fact, except for the "atomic" undefined syntax, all of the syntax axioms in set.mm can be viewed as syntactic sugar! Consider wex and wrex, for example:
wex $a wff E. x ph $. wrex $a wff E. x e. A ph $.
Notice that the "E." operator is contained in both formulas? That is typical of other set.mm syntax axioms. Norm has created a language in set.mm which is a compromise between the "pure" languages of math/logic which use polish prefix syntax and the constant/parentheses ( "(", ")" ) punctuated context-free grammars of programming languages. Unfortunately, the Metamath Proof Verification Engine algorithm cannot tolerate syntactic ambiguities, whatsoever – if "(" and ")" are used in a syntax axiom once, then they are used all of the time!
It is possible to define a context free grammar using a Metamath .mm file which really does treat ")" and "(" as grouping delimiters. But the Proof Verifier will require that a "normal" form be used; no extra or omitted parentheses can be tolerated because the Proof Verifier compares formula strings. To deal with syntactic sugar in Metamath, the Metamath specification would require modification so that input .mm formulas are parsed and converted to a normal form – and then on output/display, the normal form is converted back to some other form, probably the original.
And if you look inside set.mm, df-3or actually appears inside proofs. So if you want to treat df-3or as syntactic sugar in your 'bert dialect then you must have a way to do a Hilbert-style derivation from your proof step formulas to the original-style Metamath formulas. Which is theoretically doable…but huge, if you plan to accomplish that for every set.mm definition.
Another "whine" I have about the Ghilbert definition concept is unfolding the definitions during unification/proof verification. In mmjbert I would prefer that these algorithms not be burdened with a need for intelligence. If unfolding is required, I prefer that happen explicitly, upstream, by someone/something smarter.
Really, I think, what the goal is for the Ghilbert definition feature is something which I would term "sub- formulas". Here is how I would describe "sub-formulas"…
Say we have a "term" which is repeated in many places in a proof, such that it is tedious to write and hard to look at (except by the original author who has the stuff hardwired in the cerebral cortex…) For example, say your are working on "E = m * c ** 2" and you decide to call this sub-formula/expression just "Q" and then in all of your proof steps whenever you write "Q" it is understood that "Q" expands to "E = m * c ** 2". In other words, this sub-formula feature is exactly like a mmj2 "Work Variable" except that Work Variables are automatically resolved whenever the substitution information becomes available to the program, and a "sub-formula" is defined by the user and is implicitly resolved within the proof worksheet syntactically prior to all unification/verification processing.
In summary, my perspective is not that the Ghilbert way "bad", but that in Metamath's set.mm, Norm has used considerable judgement to form "hybrid" syntax objects which could be untangled to a "pure" form, and that the job of doing the untangling should not reside in mmjbert – that is something which should belong in the user interface portion of mmj3/whatever (and will need to be smart enough to figure out how to deal with df-or and df-3or in a way which is convenient for users.)
Axioms are back, in mmjbert. Again, the Ghilbert way is a good way, but it goes beyond the objectives of mmj3/mmjbert (which is to provide unparalleled quality of service to people doing Metamath.)
These are a pain in the brain, so they're gone! At least, they aren't declared in mmjbert. Variables such as "ph" and "x" belone to the user-interface space. Who cares what they're named inside the system? All we care about is their Type/Kind (e.g. wff, class, set, etc.)
Here is how to eliminate Var/VarHyp? declarations in mmjbert: assertions and formulas will use "call signatures" in exactly the same way these are used in C, Java, etc., except that we won't even both to provide argument names…just the types – which is the same way that "term"s are defined in Ghilbert.
So, every assertion and every formula will have its own "call pattern". For example (this is an illustration of the concept, not the actual implementation):
wff ax-mp(wff wff)
Inside ax-mp, the program refers to wff-1 and wff-2.
There are a few reasons for doing this. One of which is that it is a pain in the brain to have to deal with Metamath's scopes and frames when working inside a Proof Assistant. Let the program use as many wff variables as it wants, who cares? The only time we need to care is when we are exporting a Proof Worksheet back to Metamath, and in that case, if there aren't enough wff variables at the global level, then someone can deal with that manually or with a very smart program who knows how to update-in-place a .mm file.
Another reason for doing this is that we want to maximize "locality of reference" when doing parallel/distributed code. To accomplish this we want each Assertion to carry his own baggage with him so that he can function in new environments without referring back to the original context. Soooooo…
An Assertion has its own self-contained Frame ( – and we just abandon the concept of "optional variables, by the way!) For example (keeping this illustrative of the concept but not showing the actual implementation, here is the ax-mp assertion and frame:
[ |- ax-mp (wff, wff) (): [ |- .1 (wff, wff) : wi(1, 2) ] [ |- .2 (wff) : 1 ] [ |- .0 (wff) : 2 ] ( h1(1 , 2), h2(1), qed(2) ) ]
Notice that this ax-mp has its own Mandatory Variable "frame" info stating its call variable types and distinct variable requirement (none).
And notice that each Formula has its own call pattern, which is like a "mini-frame" (but without the $d's.) The idea behind this is that we really want each Formula to be a self-contained entity so that we can dispatch Formulas for unification and unification searching, etc.
Finally, be assured that there is no expectation that users would deal with these cryptic references directly. We provide the hypothetical and largely theoretical possibility of manually manipulating the mmjbert data structures, but don't intend for them to be used that way. The idea is that a .mm file will be read and converted into mmjbert file(s) – which can then be further processed by mmj3. Which leads to the next idea…
It has been observed that set.mm can be broken down and linearly arranged by Book, Chapter and Section. A "Section" is a chunk of set.mm which introduces new syntax, defines the syntax and plays around with it. A "Chapter" contains new axioms as well as new syntax. "Book" is just a somewhat arbitrary grouping of Chapters. So the Book of Logic might contain Propositional and Predicate Logic Chapters. (Logically, ax-3 should be moved down in set.mm to the place where it is first ("allowed to be") used.)
One thing I think we can achieve easily is to extract slices of information from set.mm which are "less fragile", meaning that some changes to set.mm won't wipe out what we do downstream from it.
For example, as we all know, every statement in a .mm file is assigned a sequence number which is used to prevent circular references (an entity can only use other entities with lower sequence numbers than its own.) We would like to be able to easily add theorems without altering the subsequent theorem sequence numbers (yeah, that would be nice!) So perhaps we can assign sequence numbers by math object within section, where sections are numbered 001, 002, … 99999 and 001 is the first set.mm section and 999999 is the last. Then, if Section 23 has 94 objects, we allow the user to add AT THE END of Section 23 and assign the sequence number 95. (To add in the middle of Section 23 the user would have to put the new theorem into the source .mm file and then regenerate the mmjbert files.) So, other theorems referencing the new theorem would refer to it as "23.95" – but only interally within the code…users would refer to the new theorem by name using the Proof Assistant.
The real benefit of this scheme occurs when there are 1+ million theorems in a .mm repository, and therefore, it is expensive to regenerate all of the downstream stuff… Because syntax and logical axioms rarely change or move -- they occur at the beginning of each Section – their sequence numbers are fairly durable. So it is fairly doable to determine is we need to regenerate our Grammatical Parser (or our 3D V/R avatars :-) We just output separate syntax/axiom export files and compare them to the previous version – if no change, then no need to regenerate the Grammar!!! And, if the syntax/axiom delta- data shows a change we know that there may be other manual intervention needed for downstream systems!
Here is a more detailed "vision" of how this would work:
a) Separate each "Section" into two parts, Syntax and Logic.
b) Syntax sections are assigned odd numbers, Logic even. So Section 1 is syntax, (early propositional), and Section 2 is logic, Section 3 is syntax (introduces <->), Section 4 is logic.
c) Each assertion is assigned a sequence number within its section, which is qualified by Section Number. This is tedious in usage but enables us to maintain a statement numbering scheme that can be used – internally – for subscripting into tables (if the programmer desires). So "wi" is assigned key 1.1 (or 1-1 or <1 1> … whatever) and "ax-1" is assigned key 2.1.
d) Each sub-section is written out to a separate export file as Metamath 7-bit ASCII formatted in s-expressions, and is zipped to minimize size/transmission times. A sha1 key is also generated for each zipped export file.
e) A separate file containing a list of all exported files and their sha1 keys is produced. This file may also contain parameter settings (e.g. "|-" is the theorem type), or it may contain an entry specifying a parameter/option file.
f) As a concession to brevity, Type Codes ("kinds" in ghilbert) are output without a Section Number in the export files, and are assigned sequence numbers 1, 2, 3, … Separately, a Type Code file is output which contains "pointers" to the Section where the Type Code is first introduced. (A separate set of export files will need to be defined for the Metamath grammar…and typesetting information – that is a big specification task and I defer it for this moment.)
g) The export files are available, either within a local filesystem or over a network. The sha1 checksums can be used to determine whether or not a given file needs to be re-downloaded/imported. And, the syntax assertions are split from the logic statements providing efficient access for grammar processors – plus, since we will allow statements to be added at the end of a section, it will be possible to add new syntax without altering sequence numbers of logic statements.
h) I envision adding a mmjbert extract process to mmj2, either as an integral part accessible via RunParm? commands, or as a separate program which calls the mmj2 code modules but is not loaded or referenced in any way by mmj2 users. The benefit of using mmj2 for the extract is that mmj2 does very extensive validation of each input .mm file, so if mmj2 doesn't report any errors during the file load process, then the output mmjbert files are pretty much guaranteed to be clean – this is a vitally important consideration given that one would expect the code which reads in mmjbert files to do minimal validation of its input (– just read and run.) Also, mmj2 could remain in memory available for callbacks, say, if a Proof Worksheet needed to be Unified to generate a Metamath RPN proof (in mmj2bert, as with ghilbert, the low-level format of the proofs will not exactly match the Metamath specification, so a converter to Metamath format is needed.)
i) To minimize referential (external key) lookups (as we know Metamath files are hierarchies with many intra-hierarchy references), in the export files and possibly internally in code using them, assertion references would be written out with the Type Code. So, "wi" would be written out as "1-1-2" (i.e. Section 1, statement label "wi", statement type = "wff"). And since the parse/proof trees (or s-expressions) convey the number of operands for each operator, all of the information needed for unification is conveyed as part of each statement's data – there is no need to do a lookup to find out the type code of "wi" or how many operands it has. This means that in a distributed/ parallel processing environment, little algorithms can be written to do many of the tedious tasks and those algorithms won't need access to the entire set of data structures – we'll design the export files to facilitate these tasks, and since we're using sequence numbers instead of text labels/operators, in those cases where lookups are needed, they will be direct subscript accesses!
1. To avoid dealing with "optional" variables and optional Dj Variable restrictions, the mmjbert export format proofs will consist of s-expression trees containing only the label/keys of logical assertions and hypotheses. This means that any downstream code that wishes to display or fully instantiate a proof will need to perform a unification process to generate variable substitutions to generate complete formulas for proof steps. But that is "ok" because doing unification for one proof is intricate but not a massive computational task and existing proofs are not frequently used. Also, these "macro-level proofs" are more durable and resistant to change. In fact, the mmjbert format could be used to import proofs back into mmj2.
2. Why compress mmjbert export files? Because it is faster to transport and un-zip a compressed file than to transport an unzipped file. The primary objective of mmjbert – why invest lifespan even thinking about it – is to facilitate distributed/parallel processing for Metamath databases, whether on a local cluster of multi-core processors or over the internet. For example, suppose there are 'n' possible solutions for a single proof step (e.g. we don't know which assertion to use as justification but we know that there are 'n' unifiable assertions). Then it is possible to create n proof skeletons and ship them out for processing – and those processors could operate independently and either solve the problem, or break it down and and distribute new requests.
3. Aside from typesetting information, which is of concern only for modules with external, user-oriented interfaces, there are two types of statements: syntax axioms and logic statements (logic hypotheses, logic axioms, and theorems – we can disregard syntax theorems as they are artifacts of metamath.exe and reside only inside metamath.exe generated RPN proofs.)
Now, for syntax statements and logic statements there are 'm' and 'n' attributes for each statement type. One idea which mmjbert will explore is generating use-specific export files containing only subsets of the available attributes.
The main example of this is separating actual proofs from the logic statements, based on the idea that existing proofs are rarely accessed. (The other main example is splitting the syntax and logic statements into completely different files!)
Additional situations will likely be discovered during the specification/design process. The benefits of slicing the data "rows" this way are that a) the amount of data which needs to be distributed can be minimized; b) specific processing code can be simpler, faster and more robust if not burdened with extraneous information.
4. My next step is to refine these ideas into something elegant. Get rid of words, add pictures, create file specs, etc. So far this line of attack has not generated any interest or feedback, but I believe that it will be possible to create a fun and useful project. Perhaps I can get kick the can far enough down the road so that sub-projects in distributed/parallel programming will be available for the 2009 GSOC. (Note to self: find some academic/corporate justification to back this up.)
I manually entered (chapter) and section numbers using the mmtheorems page at metamath.org. It would be interesting to see these graphed – say, on a sphere, with lightning bolts generated (and sound) from proof steps to justifying assertion…triggering chain reactions to those theorems' justifying assertions. Or, each section could be a spherical ship in orbit around a sun, with proof steps generating messages between proof steps and justifying assertions.
Table of Contents – metamath.org:8888 set.mm as of 20080518
(01) Pre-logic 0001 Dummy link theorem for assisting proof development dummylink 1 (02) Propositional calculus 0002 Recursively define primitive wffs for propositional calculus wn 2 0003 The axioms of propositional calculus ax-1 4 0004 Logical implication a1i 8 0005 Logical negation a3i 74 0006 Logical equivalence wb 146 0007 Logical disjunction and conjunction wo 222 0008 Miscellaneous theorems of propositional calculus pm5.1 673 0009 Abbreviated conjunction and disjunction of three wff's w3o 771 0010 Other axiomatizations of classical propositional calculus meredith 920 (03) Predicate calculus without distinct variables 0011 The axioms of "pure" predicate calculus wal 950 0012 The axioms for the equality predicate (except ax-10 and ax-11) cv 1098 0013 The axioms for a binary non-logical predicate wcel 1104 0014 Introduce axioms ax-11 and ax-10 ax-11 1124 0015 Substitution wsbc 1157 0016 Theorems using axiom ax-11 equs5a 1184 (04) Predicate calculus with distinct variables 0017 The axiom of quantifier introduction ax-17 ax-17 1194 0018 Derive the axiom of distinct variables ax-16 ax16 1197 0019 Derive the original axiom of variable substitution ax-11o ax11o 1205 0020 Theorems without d.v. restrictions that rely on axiom ax-11o ax11b 1208 0021 Predicate calculus with distinct variables (cont.) ax11v 1253 0022 More substitution theorems equsb3lem 1315 0023 Existential uniqueness weu 1362 (05) ZF Set Theory - start with the Axiom of Extensionality 0024 Introduce the Axiom of Extensionality ax-ext 1441 0025 Class abstractions (a.k.a. class builders) cab 1445 0026 Negated equality and membership wne 1566 0027 Restricted quantification wral 1626 0028 The universal class cvv 1791 0029 Russell's Paradox ru 1917 0030 Proper substitution of classes for sets sbhypf 1918 0031 Proper substitution of classes for sets into classes csb 1980 0032 Define basic set operations and relations cdif 2023 0033 Subclasses and subsets dfss2 2037 0034 The difference, union, and intersection of two classes difeq1 2132 0035 The empty set c0 2259 0036 "Weak deduction theorem" for set theory cif 2340 0037 Power classes cpw 2380 0038 Unordered and ordered pairs csn 2388 0039 The union of a class cuni 2480 0040 The intersection of a class cint 2510 0041 Indexed union and intersection ciun 2543 0042 Binary relations wbr 2596 0043 Ordered-pair class abstractions (class builders) copab 2643 0044 Transitive classes wtr 2657 (06) ZF Set Theory - add the Axiom of Replacement 0045 Introduce the Axiom of Replacement ax-rep 2670 0046 Derive the Axiom of Separation axsep 2679 0047 Derive the Null Set Axiom zfnuleu 2684 0048 Theorems requiring subset and intersection existence nalset 2689 0049 Theorems requiring empty set existence class2set 2711 (07) ZF Set Theory - add the Axiom of Power Sets 0050 Introduce the Axiom of Power Sets ax-pow 2719 0051 Derive the Axiom of Pairing zfpair 2754 0052 Ordered pair theorem opth 2763 0053 Ordered-pair class abstractions (cont.) opabid 2782 0054 Power class of union and intersection pwin 2797 0055 Epsilon and identity relations cep 2802 0056 Partial and complete ordering wpo 2812 (08) ZF Set Theory - add the Axiom of Union 0057 Introduce the Axiom of Union ax-un 2840 0058 Founded and well-ordering relations wfr 2888 0059 Ordinals word 2920 0060 Transfinite induction tfi 3099 0061 The natural numbers (i.e. finite ordinals) com 3104 0062 Peano's postulates peano1 3122 0063 Finite induction (for finite ordinals) find 3128 0064 Functions and relations cxp 3141 0065 Cantor's Theorem canth 3864 0066 Miscellaneous ordinal theorems (that depend on functions and relations) iunon 3866 0067 Transfinite recursion tfrlem1 3868 0068 Recursive definition generator crdg 3888 0069 Finite recursion frfnom 3908 0070 Abian's "most fundamental" fixed point theorem abianfplem 3918 0071 Operations co 3920 0072 "Maps to" notation cmpt 4029 0073 First and second members of an ordered pair c1st 4033 0074 Ordinal arithmetic c1o 4084 0075 Natural number arithmetic nna0 4179 0076 Equivalence relations and classes wer 4214 0077 The mapping operation cm 4278 0078 Infinite Cartesian products cixp 4303 0079 Equinumerosity cen 4320 0080 Schroeder-Bernstein Theorem sbthlem1 4399 0081 Pigeonhole Principle phplem1 4460 0082 Finite sets onomeneq 4470 0083 Supremum csup 4519 (09) ZF Set Theory - add the Axiom of Regularity 0084 Introduce the Axiom of Regularity ax-reg 4537 0085 Axiom of Infinity equivalents inf0 4550 (10) ZF Set Theory - add the Axiom of Infinity 0086 Introduce the Axiom of Infinity ax-inf 4566 0087 Existence of omega (the set of natural numbers) omex 4571 0088 Rank cr1 4585 0089 Scott's trick; collection principle; Hilbert's epsilon scottex 4660 0090 Axiom of Choice equivalents aceq1 4673 (11) ZFC Set Theory - add the Axiom of Choice 0091 Introduce the Axiom of Choice ax-ac 4688 0092 AC equivalents: well ordering, Zorn's lemma numthlem 4727 0093 Cardinal numbers ccrd 4757 0094 Cofinality cflem 4849 0095 Cardinal number arithmetic ccda 4861 0096 ZFC Axioms with no distinct variable requirements nd1 4882 (12) Real and complex numbers 0097 Dedekind-cut construction of real and complex numbers cnpi 4916 0098 Real and complex number postulates axaddopr 5209 0099 Real and complex numbers - basic operations cmin 5236 0100 Some deductions from the field axioms for complex numbers addclt 5245 0101 Addition add12t 5280 0102 Subtraction cnegextlem1 5289 0103 Multiplication mulid2t 5361 0104 Infinity and the extended real number system cpnf 5427 0105 Restate the ordering postulates with extended real "less than" axlttri 5447 0106 Ordering on reals lttrt 5452 0107 Ordering on the extended reals elxr 5480 0108 Ordering on reals (cont.) eqlet 5516 0109 Reciprocals ixi 5626 0110 Division df-div 5644 0111 Ordering on reals (cont.) elimgt0 5737 0112 Natural numbers (as a subset of complex numbers) df-n 5845 0113 Principle of mathematical induction nnind 5857 0114 Natural numbers (cont.) nn1suc 5859 0115 Decimal representation of numbers c2 5880 0116 Some properties of specific numbers 2p2e4 5920 0117 Completeness Axiom and Suprema lbreu 5964 0118 Supremum on the extended reals xrsupexmnf 5993 0119 Nonnegative integers (as a subset of complex numbers) df-n0 6019 0120 Integers (as a subset of complex numbers) df-z 6055 0121 Well-ordering principle for bounded-below sets of integers uzwo3lem1 6136 0122 The floor (greatest integer) function cfl 6143 0123 Rational numbers (as a subset of complex numbers) df-q 6166 0124 Positive reals (as a subset of complex numbers) df-rp 6191 0125 Monotonic sequences monoord 6203 0126 The infinite sequence builder "seq1" om2uz0 6204 0127 The "shift" operation cshi 6249 0128 Real number intervals cioo 6266 0129 Upper partititions of integers cuz 6321 0130 Finite intervals of integers cfz 6371 0131 Superior limit (lim sup) clsp 6431 0132 Infinite sequence builders "seq" and "seq0" cseqz 6435 0133 Integer powers cexp 6472 0134 Discriminant discrlem1 6558 0135 More natural number properties nnsqcl 6562 0136 Ordered pair theorem for nonnegative integers nn0le2msqt 6565 0137 Square root csqr 6571 0138 Irrationality of square root of 2 sqr2irrlem1 6626 0139 Imaginary and complex number properties irec 6633 0140 Real and imaginary parts; conjugate; absolute value cre 6650 0141 Factorial function cfa 6840 0142 The binomial coefficient operation cbc 6865 0143 Limits cli 6884 0144 Finite and infinite sums csu 6889 0145 Finite sums (cont.) dffsum 6908 0146 The binomial theorem binomlem1 6976 0147 Limits (cont.) clm1 6987 0148 Infinite sums (cont.) dfisum 7099 0149 Miscellaneous converging sequences reccnv 7125 0150 Arithmetic series fnsmntlem 7132 0151 Geometric series expcnvlem1 7134 0152 Ratio test for infinite series convergence cvgratlem1ALT 7154 0153 The product of two finite sums fsum0diaglem1 7163 0154 Continuous complex functions ccncf 7169 0155 Intermediate value theorem ivthlem1 7188 0156 The exponential, sine, and cosine functions ce 7207 0157 e is irrational eirrlem1 7302 0158 The exponential, sine, and cosine functions (cont.) abspef01tlub 7308 (13) Axiom of dependent choice (14) Cardinality and cardinal arithmetic (cont.) 0159 Countability of integers and rationals nn0ennn 7411 0160 Infinite primes theorem unbenlem 7419 0161 The reals are uncountable ruclem1 7425 0162 Cardinal arithmetic (cont.) infxpidmlem1 7467 0163 Continuum Hypothesis gch-kn 7501 (15) Topology 0164 Topological spaces ctop 7502 0165 Bases for topologies isbasisg 7525 0166 Subbases for topologies subbas 7558 0167 Examples of topologies subtop 7560 0168 Closure and interior ccld 7574 0169 Neighborhoods cnei 7623 0170 Limit points clp 7651 0171 Continuity ccn 7662 0172 Hausdorff spaces cha 7690 (16) Metric spaces 0173 Basic metric space properties cme 7698 0174 Metric space balls blfval 7745 0175 Open sets of a metric space opnfval 7767 0176 Continuity in metric spaces metcnpf 7792 0177 Examples of metric spaces cnmetdval 7811 0178 Convergence and completeness clm 7827 0179 Examples of complete metric spaces cncms 7902 0180 Baire's Category Theorem bcthlem1 7903 (17) Group theory 0181 Definitions and basic properties for groups cgr 7937 0182 Definition and basic properties of Abelian groups cabl 8005 0183 Subgroups csubg 8021 0184 Examples of groups grpsn 8031 0185 Examples of Abelian groups ablsn 8032 0186 Group homomorphism ghgrpilem1 8040 (18) Ring theory 0187 Definition and basic properties cring 8046 0188 Examples of rings cnring 8069 (19) Complex vector spaces 0189 Definition and basic properties cvc 8071 0190 Examples of complex vector spaces cnvc 8105 (20) Normed complex vector spaces 0191 Definition and basic properties cnv 8106 0192 Examples of normed complex vector spaces cnnv 8205 0193 Induced metric of a normed complex vector space imsval 8214 0194 Inner product cip 8241 0195 Subspaces css 8272 (21) Operators on complex vector spaces 0196 Definitions and basic properties clno 8293 (22) Inner product (pre-Hilbert) spaces 0197 Definition and basic properties cphl 8360 0198 Examples of pre-Hilbert spaces cnph 8367 0199 Properties of pre-Hilbert spaces isph 8370 (23) Complex Banach spaces 0200 Definition and basic properties cbn 8411 0201 Examples of complex Banach spaces cnbn 8417 0202 Uniform Boundedness Theorem ubthlem1 8418 0203 Minimizing Vector Theorem minveclem1 8434 (24) Complex Hilbert spaces 0204 Definition and basic properties chl 8478 0205 Standard axioms for a complex Hilbert space hlex 8487 0206 Examples of complex Hilbert spaces cnhl 8505 0207 Subspaces ssphl 8506 0208 Hellinger-Toeplitz Theorem htthlem1 8507 (25) Posets and lattices 0209 Definition and basic properties cps 8520 (26) Real and complex numbers (cont.) 0210 The exponential, sine, and cosine functions (cont.) sincolem 8534 0211 Properties of pi = 3.14159... pilem1 8540 0212 Mapping of the exponential function efgh 8583 0213 The natural logarithm on complex numbers clog 8621 (27) ZFC Set Theory plus Grothendieck's Axiom 0214 Introduce Grothendieck's Axiom ax-groth 8666 (28) Sandboxes for user contributions 0215 Sandbox guidelines sandbox 8673 (29) Sandbox for Paul Chapman 0216 Miscellaneous theorems lemul2itALT 8674 0217 Group homomorphism and isomorphism cghom 8682 0218 Symmetry groups and Cayley's Theorem csymgrp 8703 (30) Sandbox for Jeff Hoffman 0219 Interfaces for finite induction on generic function values fveleq 8719 (31) Sandbox for Frederic Line 0220 Propositional and predicate calculus ahypfmbi 8723 0221 Basic Set theory ntunte 8736 0222 Finite intersection stuff using function fi cfi 8766 0223 Intervals of reals and of extended reals iooirrsa 8773 0224 Euclidean topology ceuctop 8781 0225 Neighborhoods esnnei 8787 0226 Homeomorphisms chomeosm 8788 0227 Initial and final topologies csubsp 8814 0228 Filters cfil 8818 0229 Limits cflim2 8839 0230 Separated spaces: T0, T1, T2 (Hausdorff) ... ct0 8841 0240 Connectedness ccon 8851 0241 Standard topology on RR clicls 8853 0242 Pre-calculus and Cartesian geometry dmse1 8854 0243 Standard topology of intervals of RR stoi 8870 0244 Directed multi graphs cmgra 8871 0245 Category and deductive system underlying "structure" calg 8874 0246 Deductive systems cded 8898 0247 Categories ccat 8916 0248 Homsets chom 8944 0249 Monomorphisms, Epimorphisms, Isomorphisms cepi 8962 0250 Functors cfunc 8975 0251 Tarski's classes and ranks csubcl 8981 (32) Sandbox for Steve Rodriguez 0252 Hypergraphs chgra 8984 0253 Examples of hypergraphs emhgrat 8994 0254 Pseudographs cpgra 8996 0255 Simple graphs csgra 8999 (33) Humor 0256 April Fool's theorem avril1 9001 (34) Hilbert Space Explorer 0257 Vector space postulates for a Hilbert space ax-hilex 9054 0258 Vector operations hvmulex 9066 0259 Inner product postulates for a Hilbert space ax-hfi 9132 0260 Inner product his5t 9139 0261 Norms df-hnorm 9174 0262 Relate Hilbert space to normed complex vector spaces hilabl 9213 0263 Bunjakovaskij-Cauchy-Schwarz inequality bcsALT 9232 0264 Cauchy sequences and limits df-hcau 9237 0265 Derivation of the completeness axiom from ZF set theory hilmet 9249 0266 Completeness postulate for a Hilbert space ax-hcompl 9259 0267 Relate Hilbert space to ZFC pre-Hilbert and Hilbert spaces hhcms 9260 0268 Subspaces df-sh 9264 0269 Closed subspaces df-ch 9280 0270 Orthocomplements df-oc 9312 0271 Projection theorem projlem1 9362 0272 Projectors df-pj 9412 0273 Orthomodular law omlsilem 9419 0274 Projectors (cont.) pjtheu2 9425 0275 Subspace sum, span, lattice join, lattice supremum df-shsum 9448 0276 Hilbert lattice operations sh0let 9539 0277 Span (cont.) and one-dimensional subspaces spansn0 9639 0278 Operator sum, difference, and scalar multiplication df-hosum 9683 0279 Commutes relation for Hilbert lattice elements df-cm 9703 0280 Foulis-Holland theorem fh1t 9738 0281 Quantum Logic Explorer axioms qlax1 9745 0282 Orthogonal subspaces osumlem1 9755 0283 Orthoarguesian laws 5OA and 3OA 5oalem1 9776 0284 Projectors (cont.) pjorth 9791 0285 Mayet's equation E_3 mayete3 9850 0286 Zero and identity operators df-h0op 9851 0287 Operations on Hilbert space operators hoaddclt 9861 0288 Linear, continuous, bounded, Hermitian, unitary operators and norms df-nmop 9942 0289 Linear and continuous functionals and norms df-nmfn 9948 0290 Adjoint df-adjh 9952 0291 Dirac bra-ket notation df-bra 9953 0292 Positive operators df-leop 9955 0293 Eigenvectors, eigenvalues, spectrum df-eigvec 9956 0294 Theorems about operators and functionals nmopvalt 9959 0295 Riesz lemma riesz3 10170 0296 Adjoints (cont.) cnlnadjlem1 10175 0297 Quantum computation error bound theorem unierr 10210 0298 Dirac bra-ket notation (cont.) branmfnt 10211 0300 Positive operators (cont.) leopg 10227 0301 Projectors as operators pjhmop 10244 0302 States on a Hilbert lattice df-st 10309 0303 Godowski's equation golem1 10368 0304 Covering relation; modular pairs df-cv 10376 0305 Atoms df-at 10433 0306 Superposition principle superpos 10449 0307 Atoms, exchange and covering properties, atomicity chcv1t 10450 0308 Irreducibility irredlem1 10485 0309 Atoms (cont.) atcvat3 10491 0310 Modular symmetry mdsymlem1 10498
FYI, if you ever want to automate this, here is the algorithm the metamath program uses. It is basically an ad-hoc, informal "standard" based on the characteristics the set.mm program happened to have when I added the theorem list command.
MM> help write theorem_list ... The first output file, "mmtheorems.html", includes a Table of Contents. An entry is triggered in the database by "$(" immediately followed by a new line starting with either "#*#*" (for a section break) or "=-=-" (for a subsection break). The line following that one that will be used for the table of contents entry, after trimming spaces. In between two successive statements that generate web pages (i.e. $a and $p statements), only the last section and/or subsection break will be used, and any subsection break before a section break will be ignored. See the set.mm database file for examples.
[Warning: For matching, white space is NOT ignored. There should be no spaces between "$(" and the end of the line. This may be allowed in a future version, if a request is made to N. Megill.]
– norm 20 May 2008
Thanks. Whitespace ought to be whitespace. I suggest modifying the criteria so that if the first token of a comment's content (exclusive of the '$(' token) begins with "#*#*#*#*" then that indicates a section break, and likewise for sub-sections.
Also, it looks like "Axiom of dependent choice" is missing a sub-secion break. In that case the sub-section title defaults to the section title, yes?
Also, I wonder if you might not want to add a break element for Volume – Preliminaries, Propositional, Predicate, Set Theory, blah-blah.
Furthermore, I like the nomenclature: Volume, Chapter, Section.
Lastly, somewhat unrelated, I wonder if "Sandbox" is diminutive and could be changed to "Truth Mine" or "Mining Claim". To me, a sandbox is a place for children or cats to do business :-)
And, should the Sandbox sections be at the end of set.mm? That way it is simple to exclude them from load processes which specify a single endpoint.
P.S. I now see that the next logical mmj2 project is creation of an Interface interface for exporting data. In practice export code would be in separate load modules and not part of the regular mmj2 download. Dynamically loaded via RunParm? request and passed references to the entire set of mmj2 goodies: StmtTbl?, SymTbl?, Proof Verifier, Grammar, Proof Assistant, etc. Plus, mmj2 needs to be modified to load – optionally, upon RunParm? request – more stuff from a .mm file, including typesetting info, Chapter/Section numbers/titles, Begin/End Scope statements, and additional comments (for axioms, etc.) This is necessary because export format requirements cannot be fully specified in advance. And, having the facility in place will make it super easy for future programmers to access .mm databases in pre-parsed, pre-validated mode. --ocat 21-May-2008