Hi all,
A few months ago, after the discussion here on bundling with Mario, I
experimented removing dependencies on ax-13 from many theorems. This is in
my mathbox, in the section titled
21.29.4.12 Removing dependencies on ax-13 (and ax-11)
(beginning with http://us2.metamath.org/mpeuni/bj-axc10v.html) which has a
detailed section (head) comment.
It is of course known and trivial that one can remove dependency on ax-13
by adding dv conditions among setvar variables, since ax-13 itself can be
proved from previous axioms when adding two such dv conditions (this is
ax13w). What came to me as a surprise is how easy it is to actually carry
out this program in practice: one only has to prove a few (maybe a hundred
or so) of the technical lemmas following ax-13 with added dv conditions,
and then most of the later theorems can be proved without requiring ax-13
and without adding dv conditions. This is because these hundred-or-so
technical lemmas are mainly used later with dummy variables, which can
always be considered disjoint.
Basically, what I did "semi-automatically" and without much thinking, was:
starting at ax-13 and following the same order as in the main part, prove
all the theorems and label/comment them as follows (say the original
theorem is xxx):
- if it requires extra dv conditions:
bj-xxxv : Version of xxx with a dv condition, which does not require
ax-13,
- if it requires no dv conditions:
bj-xxx : Remove dependency on ax-13 from xxx.
For the moment, there are around 60 of each. The section "1.5.4 Axiom
scheme ax-13 (Quantified Equality)" has 242 theorems (counting everything),
and after that point, more and more theorems will fall in the second
category, "automatically".
I would propose moving most of these to the main part. This would be
transparent to nearly all more advanced theorems, and this would remove
dependencies on that axiom.
Recently, Wolf has made similar improvements, which is why I'm writing now
to give some update and get some opinions. Actually, it seems to me that
Wolf made the remarkable achievement of going through *all* the theorems,
starting at the very beginning, and shortening the proofs of many of them,
dropping some axiom dependencies on the way, and that now he's around the
2000^th theorem ! His approach is more carefully crafted than my
semi-automatic approach. Please Wolf, continue doing so, keeping the older
proofs as xxxOLD, or xxxALT if you deem it worth.
The two approaches are certainly not exclusive, in my opinion. Mine would
remove dependencies on ax-13 more systematically and without much human
thinking, but it would add around a hundred more theorems to the FOL part
of set.mm (I see no drawback to it, but some are more reluctant).
Benoît
--
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/b9d4af26-4e12-4ac5-9d41-07af7217fba9%40googlegroups.com.
