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). On December 1, 2019 2:24:25 PM PST, Benoit <[email protected]> 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/b9d4af26-4e12-4ac5-9d41-07af7217fba9%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/F370A55C-AC68-4F64-B5BD-2D583C201C70%40panix.com.
