Well it's redoing a lot of the work that exists in set.mm, and you can't really share results across them. For most logical subsystems, we address it directly in set.mm by using more itemized axioms and leveraging the "this theorem was proved from axioms:" list for tracking so that all the subsystems can transparently coexist. When the axiomatic system is significantly different and/or inconsistent with set.mm, it has to be developed in a separate database (like hol.mm or nf.mm), but iset.mm does not look like that to me, it uses variables and binding and all of the other structural things in exactly the same way, it just omits some logical axiom and replaces it with weaker things. Given a free choice I think that developing in the same database is better since then intuitionistic proofs can be used in classical theorems (and vice versa, when the classical theorem was not actually using classical logic on accident or because of a refactor).
On Sun, Mar 10, 2024 at 9:16 AM Gino Giotto <ginogiotto.giap...@gmail.com> 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). > > 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 kin...@panix.com > 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 <di....@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 <ginogiott...@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+u...@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+u...@googlegroups.com. >> >> 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/abbbe986-6a42-4a69-a34b-5b1639977cc1n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/abbbe986-6a42-4a69-a34b-5b1639977cc1n%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/CAFXXJStTDLXOXEOT5CcHihfEJwyY4uYLb61gDcuggF72svfCLA%40mail.gmail.com.
