And of course the largest such refactor in this vein is iset.mm, although this one was considered sufficiently different as to be moved to a separate database (which I think is slightly unfortunate).
On Tue, Jan 9, 2024 at 10:17 PM Mario Carneiro <di.g...@gmail.com> wrote: > IMO this is definitely worthwhile, especially since it moves an axiom from > used almost everywhere to used almost nowhere. We have previously done > refactors of that kind for ax-groth, ax-ac2, ax-reg, ax-rep and I think we > have a better understanding of the true dependencies of many theorems as a > result. > > On Tue, Jan 9, 2024 at 9:30 PM Gino Giotto <ginogiotto.giap...@gmail.com> > wrote: > >> I believe the question now is whether there is a general consensus for >> eventually bringing set.mm towards this direction. Is low usage of ax-13 >> at the cost of more than 100 additional lemmas what we wish for? Or maybe >> you would like to follow different paths and pursue different achievements? >> Looking forward to hear your thoughts. >> >> Il giorno mercoledì 3 gennaio 2024 alle 02:02:21 UTC+1 Benoit ha scritto: >> >>> Thanks Gino, I'm going to have a look. In addition to my post on the >>> discussion group that you mention, I also began to do in my mathbox what >>> you described, i.e., adding enough DV conditions to the technical lemmas so >>> as to later remove some ax-13 usages, but less systematically. Some >>> theorems made it to the main sections, but most remain in my mathbox, in >>> the section "20.15.4.12 Removing dependencies on ax-13 (and ax-11)", which >>> also has a section head comment to explain the principles. The plan was to >>> move to Main only the ones that had the greatest benefits, but since there >>> was no clear criterion, this kind of stalled. >>> >>> Benoît >>> >>> On Tuesday, January 2, 2024 at 12:52:10 AM UTC+1 di....@gmail.com wrote: >>> >>>> On Mon, Jan 1, 2024 at 6:43 PM Jim Kingdon <kin...@panix.com> wrote: >>>> >>>>> One (historical?) note: some of what we have now is the result of >>>>> experimentation in the opposite direction - trying to figure out whether a >>>>> logical system can be built without distinct variable constraints at all >>>>> (I >>>>> think there is some reference to this in some comments or web pages). I >>>>> think the verdict was that it was possible but so cumbersome as to be >>>>> impractical (because all the distinctor antecedents need to be carried >>>>> along until the point where that variable is no longer in use, I think). >>>>> But perhaps I'm not summarizing that quite right - like I say this isn't a >>>>> topic I've been hugely engaged with. >>>>> >>>> >>>> No it's worse than that: even after the variable is done being used you >>>> still can't discharge the distinctor, it permanently sticks around. >>>> Effectively all proofs end up saying "provided there are at least N >>>> variables in the metalogic, the following theorem holds" because you >>>> actually can't prove anything about whether variables exist in this >>>> setting. This admits models where e.g. the object logic only has three >>>> variables v0 v1 v2 and so you can't write any expression containing four or >>>> more forall or exists quantifiers without being degenerate in some way, so >>>> the undischargeable assumptions that pile up are saying that the object >>>> logic is at least nondegenerate enough to perform the proof in question. >>>> >>>> >>>>> On 1/1/24 13:38, Gino Giotto wrote: >>>>> >>>>> In the last few days, I've been working on reducing the usage of >>>>> ax-13, aiming at getting the highest result with the minimum amount of >>>>> changes. The results of my findings are committed in my repository branch >>>>> https://github.com/GinoGiotto/set.mm/tree/ax-13-complete, which is >>>>> based on a version of set.mm dating back to December 13, 2023. >>>>> >>>>> This research was primarily motivated by curiosity. I read this email >>>>> from Benoit >>>>> https://groups.google.com/g/metamath/c/1wi1s6qBYqY/m/FPkPsd5oAwAJ. He >>>>> described how most theorems use technical lemmas with dummy variables and >>>>> I >>>>> became interested in checking the real extent of this. The good news is >>>>> that ax-13 can be erased almost everywhere. The bad news is that I needed >>>>> 129 lemmas to accomplish this task, which is higher than the final >>>>> estimates provided in that conversation (100 seemed to be the upper >>>>> bound). >>>>> >>>>> The approach I pursued goes as follows: Starting from >>>>> https://us.metamath.org/mpeuni/ax13w.html, I proved all theorems in >>>>> the ax-13 section by adding the necessary dv conditions. Then I continued >>>>> to the "Uniqueness and unique existence" section and the first few set >>>>> theory sections until usage of proofs with dummy variables became >>>>> prevalent. Distinguishing between the theorems that require additional dv >>>>> conditions from those that don't isn't straightforward, so at first I >>>>> simply proved them all and later I pruned away those that didn't >>>>> necessitate additional dv conditions. >>>>> >>>>> This process resulted in more than 300 additional lemmas, which I >>>>> later pruned again by eliminating unused and already existing ones. This >>>>> job ultimately reduced the number to 129 additional lemmas, which I >>>>> believe >>>>> cannot be lowered further unless proof lenghtenings are introduced. >>>>> >>>>> In the meantime, I conducted multiple minimization sessions with the >>>>> new lemmas using the /MAY_GROW option. This option allows to replace steps >>>>> even when the proof length increases. In most of my minimizations, the >>>>> overall proof shape and length remained unchanged as I replaced theorems >>>>> with identical versions with more dv conditions. >>>>> >>>>> All and only my 129 additional lemmas have a *(Contributed by Gino >>>>> Giotto, 30-Dec-2023.) *tag, so this information can be used to >>>>> distinguish them from the other theorems in the database. >>>>> >>>>> I adopted the naming convention of adding a *w suffix to the original >>>>> theorem names. The reason I did not use a *v suffix is because it would >>>>> have resulted in 17 naming collisions. Since all the pre-exisiting >>>>> versions >>>>> have more dv conditions than mine, they would have to be renamed with *vv, >>>>> which would have increased the amount of changes in the commit. Also I >>>>> believe it makes sense to name them as *w since they all originated from >>>>> ax13w (even tho after shortening their proofs they don't use ax13w >>>>> anymore). So in the end, by using a *w suffix, no naming collision was >>>>> generated. >>>>> >>>>> But enough rambling, let's get to the numbers: >>>>> As of commit >>>>> https://github.com/metamath/set.mm/tree/5228c50ed1c4f3e7c41dd0d5fe49c91f5c7725c8 >>>>> dating >>>>> back to December 13, 2023, ax-13 was used by 32,347 out of 41,652 >>>>> theorems, >>>>> covering 77.66% of the entire database. As of January 1, 2024, this >>>>> percentage is at 77.64%, so it hasn't changed much since then. >>>>> >>>>> In my branch https://github.com/GinoGiotto/set.mm/tree/ax-13-complete, >>>>> thanks to the lemmas I added and the minimizations I performed, ax-13 is >>>>> used by only 819 theorems out of 41,781, which is just 1.96% of the entire >>>>> database. If we exclude OLD/ALT versions then the number of theorems that >>>>> use ax-13 goes down to around 700. The majority of these remaining >>>>> theorems >>>>> are found in the ax-13 section, in the "Alternate definition of >>>>> substitution" section, and within mathboxes. Many of those 700 theorems >>>>> could drop ax-13 by adding dv conditions directly to them, but I believe >>>>> that would be considered cheating (I only did this for 2 or 3 theorems >>>>> where adding a new version didn't seem worth it, also they didn't affect >>>>> the dv conditions of later theorems). >>>>> >>>>> It's possible to check these numbers with *metamath-knife set.mm >>>>> <http://set.mm> --stmt-use use.txt ax-13 *which shows what theorems >>>>> in set.mm use ax-13. A comparison between axiom usage of my branch >>>>> https://github.com/GinoGiotto/set.mm/tree/ax-13-complete and the base >>>>> branch >>>>> https://github.com/GinoGiotto/set.mm/tree/5228c50ed1c4f3e7c41dd0d5fe49c91f5c7725c8 >>>>> shows >>>>> the result of my minimizations. The command metamath-knife set.mm -X >>>>> ax.txt can be used to check that other axioms haven't been added, >>>>> however it's better to find a way to ignore ax-13 for this, otherwise >>>>> you're going to be overwhelmed by the amount of changes from it. So far >>>>> I've not yet seen axioms that have been mistakenly introduced (on the >>>>> contrary there are a few theorems with a reduced usage of ax-10, ax-11 and >>>>> ax-12). >>>>> >>>>> Unfortunately, despite my efforts to make as few changes as possible, >>>>> the commit on my branch6fc6153 >>>>> <https://github.com/metamath/set.mm/commit/6fc6153e0e4df76bf73bfeef76151d5354bc972c>still >>>>> looks huge, with about 48,000 changed lines. Most of these changed lines >>>>> are the result of the minimization process and rewrapping (the proof >>>>> changes themselves are often very minor, in reality it's the rewrapping >>>>> the >>>>> skews everything). I didn't find ways to lower this number down without >>>>> tradeoffs. >>>>> >>>>> This result (aka the mentioned branch in my fork) can be used in >>>>> different ways, one could use it as a simple consultation for future axiom >>>>> minimizations, or maybe it can be converted into a proper PR series. The >>>>> latter would require some non-trivial work of systematization, so probably >>>>> it would be better to discuss about it first. >>>>> >>>>> Regards >>>>> >>>>> Gino >>>>> -- >>>>> 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/84b387ba-298f-4252-8c70-821e3a23d372n%40googlegroups.com >>>>> <https://groups.google.com/d/msgid/metamath/84b387ba-298f-4252-8c70-821e3a23d372n%40googlegroups.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>>> -- >>>>> 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/4d7b01cb-fca5-4713-9dad-308941403db8%40panix.com >>>>> <https://groups.google.com/d/msgid/metamath/4d7b01cb-fca5-4713-9dad-308941403db8%40panix.com?utm_medium=email&utm_source=footer> >>>>> . >>>>> >>>> -- >> 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+unsubscr...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/1d10fb5c-6d2b-4b5b-bf3b-1207af44b2fcn%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/1d10fb5c-6d2b-4b5b-bf3b-1207af44b2fcn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStNwoXiaAp0nmQo3FH-UwKxr956j_pK-n8RTpKwFqGU5w%40mail.gmail.com.
