Removing dependencies on ax-13

[Benoit]

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

[Jim Kingdon]

I'm all for this, based on my experience proving a number of these theorems in iset.mm and my general impressions that the "can you build a usable system without distinct variable constraints?" work gave something a bit closer to a "no" than a "yes".

Whether it involves 100 permanently new theorems, or whether those 100 would end up replacing existing theorems rather than adding to them (after a transition period, I guess), is I suppose my biggest question (but not one that would necessarily need to be answered up front).

I noticed that http://us2.metamath.org/mpeuni/bj-equs5v.html can be replaced by the existing http://us2.metamath.org/mpeuni/sb56.html . If there a lot of things like this (I only browsed very briefly, did not go over everything), the number of new theorems might end up being a less than you think.

You also may want to compare with iset.mm, because (a) iset.mm by necessity reduced its reliance on distinctors relative to set.mm (because of the inability to do case elimination on whether two variables are distinct or not), and (b) eliminating uses of the ax-13 analogues in iset.mm may be especially appealing (I guess because they are particularly strong, or at least strong-looking, in terms of being stated as disjunctions).

[David A. Wheeler]

> On December 1, 2019 2:24:25 PM PST, Benoit <benoit...@gmail.com> 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.

In general we encourage removing dependencies on axioms.
I don't see why it would be different in this case.

--- David A. Wheeler

[Norman Megill]

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

[Benoit]

Thanks for your suggestions.  In any case, I do not plan to move anything to the main part before the end of 2019, so we still have time to discuss.

As for Jim's remarks: in your specific example, sb56 currently requires ax-13, whereas bj-equs5v (and bj-sb56) do not.  But I see a shorter way to prove bj-sb56 now, using fewer extra lemmas.  And there probably are other examples.  Indeed, I did not try to optimize things and I did "mass imports" from time to time.  As for iset.mm: it might be more interesting, for the two good reasons you mention.

Norm: you're right: the estimate of a hundred or so additional theorems is probably more of an upper bound. I already noticed a few redundancies in the "section comment"; quoting:

    Update: it turns out that several theorems of the form bj-xxxv, or minor variations, are already in set.mm with label xxxw.

And if/when I move them to the main part, some other redundancies will certainly appear, so in total there may be only a few dozen extra lemmas (and this would remove dependency on ax-13 from a few thousand theorems probably, when the program is finished). As you write, we will then decide for each lemma whether it should be an addition or a replacement.

Indeed, removing dependencies on ax-11 is also interesting (actually: more interesting, since it cannot be done in an automatic way like for ax-13). I did it for a few theorems but at the cost of adding some dv conditions, so it's not a big success.  As you said, a theorem should be moved as early as possible with respect to the axioms it requires.

Benoît