Results about ax-13 usage

[Gino Giotto]

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 --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 branch6fc6153still 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

[Jim Kingdon]

This isn't something I'm likely to get hugely involved with myself, but it does intrigue me particularly from the point of iset.mm.  There right now we have both https://us.metamath.org/ileuni/ax-bndl.html and https://us.metamath.org/ileuni/ax-i12.html (stronger and weaker forms of what in set.mm is ax-13) and ongoing discussions of what to do with them, for example at https://github.com/metamath/set.mm/issues/3711

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.

--
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.

[Mario Carneiro]

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 --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 branch6fc6153still 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.

--
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.

[Benoit]

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

[Gino Giotto]

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.

[Mario Carneiro]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1d10fb5c-6d2b-4b5b-bf3b-1207af44b2fcn%40googlegroups.com.

[Mario Carneiro]

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).

[Jim Kingdon]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStNwoXiaAp0nmQo3FH-UwKxr956j_pK-n8RTpKwFqGU5w%40mail.gmail.com.

[Gino Giotto]

> 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).

[Mario Carneiro]

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).

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/abbbe986-6a42-4a69-a34b-5b1639977cc1n%40googlegroups.com.

[Jim Kingdon]

On 3/11/24 04:32, Mario Carneiro wrote:

> 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).

If this is just a hypothetical question I guess we don't really need to
come up with a definitive answer, but I will say that if we want to keep
some of our other values (like preferring short proofs), we'd end up
with a lot of ALT theorems or other ways in which there is a classical
proof, there is an intuitionistic proof, and the intuitionistic proof is
much longer. The examples which come to mind are summation (where the
iset.mm DEFINITION has a decidability condition and other changes), the
recursion theorem, and Bézout's theorem, but there probably are others.
Note that because these are foundational results which a lot of other
things build on, if you want the list of axioms used to be informative,
you need the main proof to be the longer intuitionistic one.

Proof length aside, I guess I'm just not sure that set.mm would read
very nicely if it needed to concern itself with decidability, apartness,
additional conditions on things like supremums and convergence, etc. Not
to mention topology which beyond a certain point falls apart unless you
switch from point-set topology to locales (or so I read, iset.mm hasn't
really gotten that far yet).

I'll also say that I do agree about the observations about how iset.mm
and set.mm are similar enough that it is also awkward, in different
ways, to keep them separate. There are a lot of theorems which can
simply be copy-pasted in one direction or the other.

[Marshall Stoner]

I’m actually working on what I would like to call a “teaching” database, that unlike set.mm, allows one to separate out theorems that use the excluded middle.  I start from the same Hilbert system as set.mm, but derive a set of natural deduction rules that serve as a new set of axioms.  The derived natural deduction rules are “bottleneck”, e.g. once I have all the ND rules for propositional logic, I no longer use first 3 axioms (or MP), nor anything derived from them before the introduction of the new rules.  I’m currently working on the predicate logic section.

Because I’m designing my database to go along with a companion pdf book, it has a different philosophy than set.mm.  I use a different naming system and try to keep the number of theorems minimal as possible. I also go for the easiest proof even when it uses more axioms.  

It isn’t really a replacement if set.mm, but an attempt to combine set.mm with iset.mm would probably follow the same kind of foundation.  

It’s inconvenient to share right now as I’m on my phone, but the file is still small enough I can attach if anyone is interested.  I don’t have a git hub account yet.

Sent from my iPhone

On Mar 11, 2024, at 7:32 AM, Mario Carneiro <di....@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStTDLXOXEOT5CcHihfEJwyY4uYLb61gDcuggF72svfCLA%40mail.gmail.com.

[Mario Carneiro]

On Mon, Mar 11, 2024 at 11:36 AM Jim Kingdon <kin...@panix.com> wrote:

If this is just a hypothetical question I guess we don't really need to
come up with a definitive answer, but I will say that if we want to keep
some of our other values (like preferring short proofs), we'd end up
with a lot of ALT theorems or other ways in which there is a classical
proof, there is an intuitionistic proof, and the intuitionistic proof is
much longer.

We already have a caveat in the proof shortening rules for this. We want shorter proofs but *only* assuming it doesn't take the theorem out of a "subsystem of interest". For the most part that means that proof searches using MINIMIZE will add /NO_NEW_AXIOMS to ensure that intuitionistic proofs stay intuitionistic. So in the variation you are talking about I would expect there to only be an intuitionistic proof, and the classical proof (if the statement is different) would be the shorter of "do the proof directly" and "apply the intuitionistic version and remove the unnecessary assumptions", which probably would end up with the latter most of the time.

 

Proof length aside, I guess I'm just not sure that set.mm would read
very nicely if it needed to concern itself with decidability, apartness,
additional conditions on things like supremums and convergence, etc. Not
to mention topology which beyond a certain point falls apart unless you
switch from point-set topology to locales (or so I read, iset.mm hasn't
really gotten that far yet).

This is a fair criticism. For those areas like topology where it's still unclear how to intuitionize it, the whole thing would simply be classical. But I would expect a cover-to-cover reader of set.mm to already know that it is trying to simultaneously cover intuitionistic and classical logic, and the abstractions that work in intuitionistic logic are also interesting in their own way. I know I had to search far and wide for proofs about measure theory in the absence of the axiom of choice (thanks Fremlin!) so it wouldn't be the first time for proofs that go out of their way to avoid some axiom.

 

I'll also say that I do agree about the observations about how iset.mm
and set.mm are similar enough that it is also awkward, in different
ways, to keep them separate. There are a lot of theorems which can
simply be copy-pasted in one direction or the other.

And of course these copy-pasted theorems are a future maintenance issue, since people will have to remember to change them in tandem (or not! if the change needs classical logic) and this is hard to deal with without a global view of all the databases.

[Gino Giotto]

I announce the successful completion of the project. As of April 20, 2024, there are a total of 589 theorems that depend on ax-13, which is better than forecasted in this mailing list (back in January I anticipated 819 theorems left).

Among these 589 theorems, there are 50 "OLD" proofs in main, which will be deleted during the year. Additionally, there are 59 "ALT" theorems which may contain candidates for ax-13 removal (I generally skipped theorems with a "proof modification is discouraged" tag except for a few occurrences).

---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Below I show a summary of the locations of those 589 theorems. 400 of them are in main, and 189 in mathboxes:

* Axiom scheme ax-13 (Quantified Equality): 186 theorems

* Alternate definition of substitution: 30 theorems (it has recently been proposed to delete this section https://github.com/metamath/set.mm/pull/3924#pullrequestreview-2007403060)

* Uniqueness and unique existence: 27 theorems

* Intuitionistic logic: 6 theorems

* ZF Set Theory - start with the Axiom of Extensionality: 90 theorems

* ZF Set Theory - add the Axiom of Power Sets: 24 theorems

* ZF Set Theory - add the Axiom of Union: 2 theorems (~fsplitOLD and ~nfixp)

* ZFC Axioms with no distinct variable requirements: 31 theorems

* REAL AND COMPLEX NUMBERS: 2 theorems (~brfi1indALT and ~nfsum)

* BASIC ALGEBRAIC STRUCTURES: 1 theorem (~cygablOLD)

* GRAPH THEORY: 1 theorem (~frgrwopreglem5ALT)

-----------------END OF MAIN-------------------

* Mathbox for Thierry Arnoux: 1 theorem (~opreu2reuALT)

* Mathbox for Jonathan Ben-Naim: 3 theorems

* Mathbox for Scott Fenton: 14 theorems

* Mathbox for Anthony Hart: 1 theorem (~subsym1)

* Mathbox for BJ: 39 theorems

* Mathbox for Wolf Lammen: 53 theorems

* Mathbox for Giovanni Mascellani: 8 theorems

* Mathbox for Peter Mazsa: 1 theorem (~brabidga)

* Mathbox for Norm Megill: 15 theorems

* Mathbox for Stefan O'Rear: 4 theorems (all *OLD)

* Mathbox for Richard Penner: 5 theorems

* Mathbox for Rohan Ridenour: 3 theorems

* Mathbox for Andrew Salmon: 6 theorems

* Mathbox for Alan Sare: 24 theorems (many of these have a "proof modification" discouragement tag)

* Mathbox for Glauco Siliprandi: 2 theorems

* Mathbox for Alexander van der Vekens: 8 theorems

* Mathbox for Emmett Weisz: 2 theorems

--------------------------------------------------------------------------------------------------------------------------------------------------------------------------

All theorems in main depending on ax-13 are discouraged, which provides decent confidence that use of this axiom won't rise inadvertently. However this mechanism is not perfect, it can be circumvented by moving a theorem using ax-13 from a mathbox to main (not all theorems in mathboxes have a discouragement tag). Therefore I reccommend to manually check ax-13 usage, say, once a year.

I attached a file containing the full list of theorems utilizing ax-13, categorized by the respective chapters. You can use it to check out whether you can find further improvements in your own mathbox or in main.

[Alexander van der Vekens]

Many thanks, Gino, for your efforts. I think we have a good intermediate result now, which, however, can still be improved (manually). I will try to eliminate the usage of ax-13 in my Mathbox and the following theorems of main:

• REAL AND COMPLEX NUMBERS: 2 theorems (~brfi1indALT and ~nfsum)

• GRAPH THEORY: 1 theorem (~frgrwopreglem5ALT)

Alexander