Actually, I did make a big mistake: ∀*x*(*x* =*i* *y* ↔ *φ*) can be satisfied by a wff *φ* including a new setvar *z*, under a hypothesis implying that *z*2 = *i*. I'm not sure if there's any ∈ predicate whose left-variable instances are not "definable with parameters" in this way, at least not without the = predicate having equivalence classes of more than one distinguishable element, which is very difficult to do while satisfying ax-12. Perhaps there could be a route to proving ax-8 from cleqjust after all.
On Thu, Sep 4, 2025 at 9:57 AM Matthew House <[email protected]> wrote: > Recently, Gino Giotto posted a PR metamath/set.mm#4995 > <https://github.com/metamath/set.mm/pull/4995>, which proves ax-8 from > df-ss, and posed a question: can ax-8 similarly be proven from df-cleq? > > The justification theorem is sufficient for a definition to be > conservative, so any non-conservative result must follow from instances of > the justification theorem. Here, the justification theorem cleqjust for > df-cleq would be ⊢ (∀*x*(*x* ∈ *A* ↔ *x* ∈ *B*) ↔ ∀*y*(*y* ∈ *A* ↔ *y* ∈ > *B*)), with *A*, *B* disjoint from *x*, *y*. Each class *A* and *B* can > either be a setvar or a class abstraction. The theorem follows from axextb > if *A* and *B* are both setvars, or from eleq1ab if *A* and *B* are both > class abstractions; neither of those derivations requires ax-8. Thus, we > can assume WLOG that all uses of cleqjust are of form ⊢ (∀*x*(*x* ∈ *z* ↔ > *x* ∈ {*w* | *φ*}) ↔ ∀*y*(*y* ∈ *z* ↔ *y* ∈ {*w* | *φ*})), that is, ⊢ (∀ > *x*(*x* ∈ *z* ↔ [*x* / *w*] *φ*) ↔ ∀*y*(*y* ∈ *z* ↔ [*y* / *w*] *φ*)), > with *z*, *w*, *φ* disjoint from *x*, *y*. > > Our goal is to construct an object theory where cleqjust holds but ax-8 > does not. As in the usual interpretation, metavariables *x*, *y*, *z*, … > always represent object variables *v*0, *v*1, *v*2, …, and the truth > value of a wff depends on the values assigned to the object variables. Each > value is an ordered pair of natural numbers. The equality predicate *v**i* > = *v**j* is true iff the value of *v**i* is equal to the value of *v**j* > in both components. The membership predicate *v**i* ∈ *v**j* is true iff > *v**i* = *v**j* and the second components of both values are equal to *i*; > note how this depends on the values of *v**i* and *v**j* as well as the > index *i* of its first argument. > > Generally speaking, whenever we see "*v**i* ∈ *v**j*" in the object > theory, we should read it as *v**i* =*i* *v**j*, where each of the > predicates =0, =1, =2, … acts solely on the values of its arguments and > not the indices. To restate the definition, we have (*x* =*i* *y* ↔ (*x*1 > = *y*1 ∧ *x*2 = *i* ∧ *y*2 = *i*)). Indeed, if we wish to access some > particular predicate *x* =*i* *y* in the object theory, we can write it > as "[*x* / *v**i*] *v**i* ∈ *y*". > > Now that we have defined it, we can see that this theory easily satisfies > ax-mp through ax-7, ax-10, ax-11, and ax-13, since the connectives →, ¬, ∀, > and = all have their usual semantics. All instances of ax-12 are satisfied, > since any expansion of the wff *φ* using the ∈ predicate is equivalent to > one using some particular set of =*i* predicates, all of which respect > the semantics of =. Similarly, all instances of ax-9 are satisfied, since ⊢ > (*x* = *y* → (*v**i* ∈ *x* → *v**i* ∈ *y*)) is equivalent to ⊢ (*x* = *y* > → (*z* =*i* *x* → *z* =*i* *y*)), which is true for any =*i*. Also, all > instances of ax-ext are satisfied, since ⊢ (∀*v**i*(*v**i* ∈ *x* ↔ *v**i* > ∈ *y*) → *x* = *y*) is equivalent to ⊢ (∀*z*(*z* =*i* *x* ↔ *z* =*i* *y*) > → *x* = *y*), which is true for any =*i*. But ax-8 is not satisfied, > since ⊢ (*v*0 = *v*1 → (*v*0 ∈ *z* → *v*1 ∈ *z*)) is invalidated by the > assignment *v*0 = *v*1 = *z* = ⟨0, 0⟩. > > Finally, we want to show that all instances of cleqjust are satisfied. Any > instance will be of form ⊢ (∀*v**i*(*v**i* ∈ *z* ↔ *v**i* ∈ {*w* | *φ*}) > ↔ ∀*v**j*(*v**j* ∈ *z* ↔ *v**j* ∈ {*w* | *φ*})), with *z*, *w*, *φ* > disjoint from *v**i*, *v**j*. This can be rewritten as ⊢ (∀*x*(*x* =*i* > *y* ↔ *φ*) ↔ ∀*x*(*x* =*j* *y* ↔ *φ*)), with *y* disjoint from *x* and *φ* > disjoint from *v**i*, *v**j*. The crucial idea is that for all wffs *φ* > definable in the object language, ∀*x*(*x* =*i* *y* ↔ *φ*) never holds if > *φ* is disjoint from *v**i*. Intuitively, this is because the particular > predicate =*i* is the only one that separates *x*2 = *i* from other > possible values of *x*2; no finite combination of predicates, logical > connectives, and quantifiers can do so, unless it involves =*i*. But > directly accessing =*i* in the object theory would require writing "*v**i* > ∈ *y*", which would violate the DV condition between *φ* and *v**i*. > Thus, cleqjust is always true in the object theory, since both sides are > always false due to the DV conditions. (As a corollary, the defined > predicate *z* = {*w* | *φ*} is always false.) > > In this object theory, all instances of ax-mp through ax-7, ax-9 through > ax-13, ax-ext, and cleqjust hold, but ax-8 does not hold. Thus, there can > be no proof of ax-8 in set.mm from the rest of ax-mp through ax-13 > together with ax-ext and df-cleq. A more clever construction of ∈ might > additionally satisfy the ZFC axioms, but that would take some work. The > underlying discrepancy for why df-ss or df-in can be used to derive ax-8, > but df-cleq cannot, is that the DV conditions do not allow us to make one > side of cleqjust true and infer the other side. > > Please let me know if there are any holes in this argument, I'm no expert > in working with wacky models, especially wacky models of Metamath's > semantics. > > Matthew House > > -- 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 visit https://groups.google.com/d/msgid/metamath/CADBQv9YT%3DAaJEpDXSoB7obj72sOsSbx2HOUK6AGzJfLj3_J01Q%40mail.gmail.com.
