I think that moving these to the main set.mm before ax-13 is introduced, and also moving up anything that no longer depends on ax-13 as a consequence, is a good idea. You can go ahead and do that.
I am a little puzzled by "but it would add around a hundred more theorems to the FOL part of set.mm". Wouldn't most of these replace existing theorems, along with a few additional ones that more or less amount to "lemmas"? Or do you really need 100 additional theorems to accomplish the ax-13 removal? I understand that some dv versions would be used to eliminate ax-13 from some proofs via dummy variables, but it seems surprising we need that many. Removing dependence on ax-11 is nice too. Can they be moved before ax-11, or do they depend on ax-12? If it seems useful to swap the order of ax-11 and ax-12 in set.mm, I can go along with that (although we won't be renumbering them anymore). My work on ax-11 a couple of years ago unsuccessfully attempted to unbundle ax-11 like we did with ax-6 (where ax-6 itself has usage discouraged, and we derive ax6 from ax6v). It might be interesting to revisit this eventually if dependence on ax-11 is removed from enough theorems. I deleted the ax-11 work from my mathbox on 27 Apr 2019 (still available on github of course), but a summary of how far I got is given here (where ax-11 used to be called ax-7): https://groups.google.com/d/msg/metamath/XGylvqTLAe0/s9b9x1PPDQAJ Norm On Sunday, December 1, 2019 at 5:24:26 PM UTC-5, Benoit wrote: > > 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/674322e6-ec7d-4359-a6fb-8e5a5f1f86d6%40googlegroups.com.
