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/CAFXXJSugnctcX6kSyd0ZxLaWaVxS%2BWbBXcJg2-ZtkjjantY74A%40mail.gmail.com.
