On 10/28/21 2:20 PM, Benoit wrote: > I think we should keep the "overloading" of equality and membership. > The assumption is not hidden in set.mm, but explicit: it is ~cv > (http://us2.metamath.org/mpeuni/cv.html). I still favor the forms > bj-df-cleq/bj-dfclel, which imply minimal changes over the current > set.mm, and which fix the concrete problem of having later theorems > which misleadingly do not indicate ax-8 or ax-9 as a dependency (which > is the problem which started this thread). And Wolf, who started the > thread, seems to agree.
The hypothesis of bj-df-cleq corresponds to setvar substitutions into A and B. Do we know that other substitutions into A and B can't generate FOL= statements that are stronger than the hypothesis? Perhaps we are safe since we may need df-cleq itself to eliminate the resulting class notation, but I haven't thought it through completely to be sure there aren't tricks that can be done with the other two class definitions. What do you think? A radical solution that would guarantee complete isolation of df-cleq from FOL= would be to use a conjunction of all FOL= axioms (and ax-ext) as the df-cleq hypothesis. But that would be ugly, and we might get the opposite complaint that too many FOL= axioms become required to use df-cleq. :) Norm -- 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/30d4173c-7041-40f7-957f-1dd38c38c02fn%40googlegroups.com.
