Extremely quick answer, because I am busy at work, and have no time to think anything over: df-cleq DOES say something about x e. A although it is assumed to be primitive: If you cannot find an y with y e. A, y and A distinct, you cannot find an x in the bundled case either (x being free in A): -. x e. A (what else demands this?). I don't know whether this is of importance, like to go through this in greater detail, but this has to wait until evening. Again, it highlights that you have to be careful.
Wolf [email protected] schrieb am Mittwoch, 27. Oktober 2021 um 12:04:31 UTC+2: > On Wed, Oct 27, 2021 at 5:26 AM 'ookami' via Metamath < > [email protected]> wrote: > >> 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. > > > The term x e. A isn't supposed to have any definition, it is axiomatic, > and can mean any proposition at all. We get completeness after df-clab. > This is, roughly speaking, the "definition of 'class'": a class is a unary > predicate on sets, and this is the application operator. > > >> 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. >> > > df-clel is another instance of notation overloading, defining A e. B in > terms of x e. A. There is no primitive constructor for x e. A but let's > call it wvel for the purpose of discussion, such that wvel x A = wcel (cv > x) A; then df-clel is defining wcel in terms of wvel (which is axiomatic > and introduced along with the new sort "class"; in type theory parlance we > would say that wvel is the eliminator for "class" and cab is the > constructor). The axiom that connects these two axiomatic constructors is > df-clab. > > In the case of the empty set, the reason x e. (/) is determined is because > of the definition of the empty set, not the definition of wvel (which is > maximally generic). Since we define (/) using the constructor for "class", > i.e. (/) = {x | F.}, we obtain the theorem x e. (/) <-> F. using df-clab. > > Now, it is true that df-clel and df-cleq are doing a bit more heavy > lifting than just described because of the notation overloading. More > specifically, we need a way to prove that x e. A acts like a regular > predicate, i.e. satisfies equality on the left and right. On the right, we > get this by definition, since this is how wceq is defined (in terms of > wvel). On the left this needs to be axiomatized, like a strengthened > version of ax-8, but df-clel + notation overloading makes it derivable. > Additionally, we need to pin down what cv does; but this is because wvel x > (cv y) = wel x y by definition (because of the notation overloading). > Without the overloading, this would be considered the definition of cv, > i.e. x = { y | y e. x } (to be precise, "cv x = cab x (wel y x)") would be > "df-cv". > > Mario > > 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 >> >> <https://groups.google.com/d/msgid/metamath/1e7e79a3-c369-42a7-a2b4-d6c43b923a76n%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/702d5dd4-910b-4ac0-88d9-f9712491c77en%40googlegroups.com.
