> 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).
Why is it slightly unfortunate? (just curious, I don't know much about iset.mm). Il giorno mercoledì 10 gennaio 2024 alle 09:16:41 UTC+1 [email protected] ha scritto: > In a sense iset.mm is that sort of thing, although to state what is > probably obvious but maybe needs to be said anyway, iset.mm does not only > remove axioms relative to set.mm, it also adds axioms and modifies axioms. > On 1/9/24 19:19, Mario Carneiro wrote: > > 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 <[email protected]> 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 <[email protected]> >> 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 [email protected] >>>> wrote: >>>> >>>>> On Mon, Jan 1, 2024 at 6:43 PM Jim Kingdon <[email protected]> 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 [email protected]. >>>>>> 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 [email protected]. >>>>>> >>>>> 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 [email protected]. >>> 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 [email protected]. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJStNwoXiaAp0nmQo3FH-UwKxr956j_pK-n8RTpKwFqGU5w%40mail.gmail.com > > <https://groups.google.com/d/msgid/metamath/CAFXXJStNwoXiaAp0nmQo3FH-UwKxr956j_pK-n8RTpKwFqGU5w%40mail.gmail.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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/abbbe986-6a42-4a69-a34b-5b1639977cc1n%40googlegroups.com.
