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 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). > 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 [email protected] 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).
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.
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
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:
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).
Unfortunately, despite my efforts
to make as few changes as possible,
the commit on my branch 6fc6153still
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.
--
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].
--
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.
--
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].
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/abbbe986-6a42-4a69-a34b-5b1639977cc1n%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 [email protected].
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStTDLXOXEOT5CcHihfEJwyY4uYLb61gDcuggF72svfCLA%40mail.gmail.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 [email protected].
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/44A93795-E179-4638-BA3F-612A0680E47F%40gmail.com.
|
