I am not sure whether the complexity is a problem of operator overloading only. Let me explain why:
At the moment of df-cleq the term x e. A is still undefined, and can mean anything. It is known to be well-formed (by wcel), though, so our typical logical manipulations apply. It follows from df-clel that ( x e. A -> E. y y e. A ) with y, A distinct holds. Thus df-clel leaves the semantics of x e. A almost always undecided, the exemption being the empty set. This is a sensible, but not obvious result of the pair df-cleq and df-clel. Now lets look at how A. x ph is handled. At the time of introduction nothing is known about that operation, too. It could mean "count the x in ph and return true only iff its an even number". Axioms now narrow the semantics down. ax-gen is already sufficient to render the suggested meaning invalid. Note that df-cleq and df-clel do NOT explain x e. A, and hence are not definitions then. Their role in this particular case is that of an axiom somehow imposing a meaning on a generally undefined expression by specifying the empty set case. I remember, I had to sort out this kind of ideas a couple of years ago. In the end I was satisfied, but that was not a "10-minutes walk". Wolf [email protected] schrieb am Mittwoch, 27. Oktober 2021 um 00:44:57 UTC+2: > The stance I take in MM0 is that df-cleq is a definition, but it is > defining class equality in terms of set equality. The suspicious thing that > set.mm is doing is asserting that the two are the same by definition, > implicitly by representing x = y as wceq (cv x) (cv y). If you have two > equalities, then there is nothing odd going on in df-cleq, and you can then > prove a theorem that weq x y is equivalent to wceq (cv x) (cv y). This > theorem will require ax-ext (and presumably ax-9 as well). > > On Tue, Oct 26, 2021 at 6:07 PM 'ookami' via Metamath < > [email protected]> wrote: > >> >> >> Norman Megill wrote Tuesday, 26. Oktober 2021 at 21:46:35 UTC+2: >> >>> Which comment of Benoît you are referring to? >>> >>> In PR #2267 he described the phenomenon of the vanishing ax-9 as an >> artifact of df-cleq and further hinted to his bj-ax9 theorem. >> >> If, as you write, ax-9 is not important any more once you arrive at >> df-cleq, you may as well include it to the axiom list unconditionally. >> >> From my point of view the following aspects were important to trigger my >> initial post: >> >> 1. Does the axiom list appear to be trustworthy? And does it follow >> a consistent pattern? >> 2. While adding complexity to df-cleq may puzzle readers, vanishing >> axioms after a proof change is not better. And we have a concrete >> incident >> here. >> 3. df-cleq, and even more so df-clel, seem to be no ordinary >> definition anyway, as the right hand side does not always explain the >> definiendum in simpler terms, for example in case set variables are >> involved. It once took me quite some time to get over their recursive >> nature, and their implicit consequences. One is that you can restate 2 >> axioms directly, but only one is taken care of. >> >> I am at a loss how text books handle these issues; I never read one on >> logic. I am willing to believe that Metamath outperforms a majority of >> them. But this should be no reason for missing out an improvement, right? >> >> So far I think there is unusual complexity inherent to df-cleq, and since >> you cannot avoid people possibly be overwhelmed by it, you can at least >> syntactically take a clean stance. >> >> Wolf >> >> -- >> 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/34ea47c9-0b57-4b1c-8cc4-6e81617a3fefn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/34ea47c9-0b57-4b1c-8cc4-6e81617a3fefn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/1e7e79a3-c369-42a7-a2b4-d6c43b923a76n%40googlegroups.com.
