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