Well, like I said we first need to know that x e. A acts like a regular predicate, which in particular implies your theorem about the equivalence of the distinct and bundled cases. I believe that the strengthened ax-9 I mentioned (i.e. x = y -> (x e. A -> y e. A)) also implies this fact. set.mm is skimping out on this axiom and using df-cleq to prove it instead, which makes it a load-bearing definition which is not great.
On Wed, Oct 27, 2021 at 6:42 AM 'ookami' via Metamath < [email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/702d5dd4-910b-4ac0-88d9-f9712491c77en%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/CAFXXJSts%3DpuK9iKYUhNrEKBakarhNXVGnE%2BEUi-8s0udgoCn1A%40mail.gmail.com.
