Finer sectioning of set.mm

[benjub]

(The "finer" of the title has to be read as the opposite of "coarser".) There are a few sections in set.mm where several definitions are introduced "en masse", and then their properties proven altogether. This entangles results and makes it harder to organize them, which makes searches more difficult in huge sections (this is not an abstract concern, actually on several occasions it was painful to retrieve some results and see what depends on what, especially in the sections related to binary relations and functions). Unless there is opposition, I will try and untangle them, and organize them into subsections (slowly, one section at a time, and giving a heads up here before each PR). A fourth level of nested sectioning was introduced a few years ago, and this will allow this finer sectioning. In some cases, additional nesting will not be necessary, and it will be more natural to "flatten" the TOC. I did this for a few sections in the past, and recently a huge work was done by @wlammen to organize conjunction and disjunction into separate sections (see https://us.metamath.org/mpeuni/mmtheorems.html#dtl:1.2) and one can see the benefits, or at least the absence of disruption if your work is on more advanced parts.

I will begin small: I plan to organize the section introducing the unique existential quantifier and the at-most-one quantifier into two subsections. One caveat: I plan to introduce first the at-most-one quantifier, and then the unique existential quantifier, defined as the conjunction of existence and uniqueness (that is, make https://us.metamath.org/mpeuni/mo2v.html the definition of the at-most-one quantifier and https://us.metamath.org/mpeuni/eu5.html the definition of the unique existential quantifier), and make the current definitions theorems. This is more natural than the current definition of at-most-one as "existence implies unique existence" (just think of your usual ways of proving unique existence and of proving uniqueness). This will probably go with a slight shortening of the combined proof length.

Any thoughts?

(edit: corrected the worst typo ever... thanks @david-a-wheeler !)

[david-a-wheeler]

I like this idea in general. Thank you for being willing to do it.

There may be a few cases where it's easier to introduce a pair of ideas, or a small set. So I suggest starting with areas where they are obviously entangled in an unnecessary way. As always, please do the untangling in separate pull requests, so if there's an agreement on one and not the other, we can immediately accept the one and focus discussion on the other.

Unless there is opposition, I will try and entangle them

I presume you mean "untangle" here :-).

No opposition here.

[wlammen]

I remember NM opposed the idea of starting with df-mo with 'This will add df-mo to the list of used definitions practically everywhere'. Maybe df-mo in isolation is not a big deal, but blowing up this list by similar restructurings is something that has to be considered

[benjub]

Currently, one has:

MM> sh us df-mo/rec
Statement "df-mo" directly or indirectly affects the proofs of 30604 statements:
MM> sh us df-eu/rec
Statement "df-eu" directly or indirectly affects the proofs of 31080 statements:

There are currently 484 proofs using df-eu but not df-mo, so the change I propose would bring the total from 30604 to 31088 (and conversely, the number of proofs requiring df-eu may very slightly decrease). Not a big change, I would say. (And even if it was, definitions are meant to be used anyway.)

edit: @wlammen, did it answer your worries ?

[benjub]

@wlammen : is this ok for you, given the above data ?

[wlammen]

You asked for 'Any thoughts?' I am not in particular opposed to swapping df-eu and df-mo in the definition order. I pointed to a general idea Norm once expressed in this context, and I think, one has to watch out for possible negative side-effects. My personal threshold for intervening is not reached by this change. Thanks for evaluating the exact amount of changes.

[avekens]

Since I was the one who asked for a fourth level of nested sectioning (see https://groups.google.com/g/metamath/c/QQyCgQmd40U/m/AO3Vrr-6AQAJ), and also requested to split the formerly combined section "Functions and relations", I fully support Benoît's proposal of a finer sectioning in principle. I can remember, however, an argument of Norm not to use the fourth level to a larger extend: I think it was that the TOC could become to huge and incomprehensible (unfortunatly, I cannot find his statement in any place...).

[avekens]

A good next candidate of a section to be untangled could be " 2.1.5 Restricted quantification": this section contains 4 definitions, about 300 theorems, and corresponds to the nonrestricted quantifications which were restructured recently.

[benjub]

I can remember, however, an argument of Norm not to use the fourth level to a larger extend: I think it was that the TOC could become to huge and incomprehensible (unfortunatly, I cannot find his statement in any place...).

That concern can be addressed by collapsible TOCs, which are possible using HTML/CSS only (that is, no javascript needed). This would require a change in the HTML-generation part of metamath.c. Currently, the page https://us.metamath.org/mpeuni/mmtheorems.html has two parts: a TOC summary, giving two nesting levels, whose entries link to a detailed TOC, giving all four nesting levels. This is sufficient to me but this may be subjective.

Four levels do not seem too much to me, especially for a reference work that aims at the same time to be encyclopedic and to go into the finest details. For instance, LaTeX permits seven nesting levels: part, chapter, section, subsection, subsubsection, paragraph, subparagraph.

[benjub]

A good next candidate of a section to be untangled could be " 2.1.5 Restricted quantification": this section contains 4 definitions, about 300 theorems, and corresponds to the nonrestricted quantifications which were restructured recently.

Yes! I think it would be nice to define them in the FOL part, since they are not necessarily set-theoretic: the predicate $\in$ is introduced in FOL as "the binary predicate" since at that point, it can be any binary predicate. Then, for instance, A. x e. A ph simply means "for any x related to A, one has ph". Many statements in the restricted quantification section do not require ax-ext or df-clab, df-cleq, df-clel, df-nfc, df-v (see https://us.metamath.org/mpeuni/bj-ralcom4.html and nearby theorems). So maybe create a section "1.7 Restricted quantification" with four subsections ?

(Note that the sectioning for df-mo/df-eu is not finished, but I'm still on it and this can advance independently.)