And of course the largest such refactor in this vein is iset.mm
<http://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 <http://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
<http://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 <http://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 <http://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>.
