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
--
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/2401c907-1b52-40a0-8010-f905c98a63e1%40googlegroups.com.
