Looking into it further, I think the counterexample can be salvaged with a different model. Let the set of values be the non-integer rationals ℚ \ ℤ, let "vi = vj" have the usual meaning, and let "vi ∈ vj" be true iff vi < vj XOR vi < i. As before, each "∈i" instance of the predicate is distinct, so ax-8 is still false, but each instance respects equality, so ax-9 and ax-12 are still true. This time, ax-ext also holds, since ∀vi(vi ∈ x ↔ vi ∈ y) ⇔ ∀z(z ∈i x ↔ z ∈i y) ⇔ ∀z((z < x ⊻ z < i) ↔ (z < y ⊻ z < i)) ⇔ ∀z(z < x ↔ z < y) ⇔ x = y.
We finally want to show that ∀x(x ∈i y ↔ φ) is universally false for all definable φ distinct from vi, so that these instances of cleqjust are vacuously true. If φ were equivalent to x ∈i y, then for all ε sufficiently small, φ must be true for exactly one of x = i − ε or x = i + ε. But since φ cannot name ∈i directly (due to the DV condition), it cannot separate i − ε from i + ε in this way. This time, using constant setvars as parameters cannot not help in the neighborhood of x = i, since no setvar can have an integer value. (If we wanted to formally show this in another way, we could represent definable predicates φ as finite unions of polytopes in (ℚ\ℤ)n, then inductively show that no construction can lead to x = i as a bounding hyperplane. The only tricky part would be the ∀ connective.) Thus, ∀x(x ∈i y ↔ φ) cannot be true for any φ satisfying the DV conditions of cleqjust, and df-cleq cannot be used to prove ax-8 from the rest of the axioms up to ax-ext. On Fri, Sep 5, 2025 at 10:38 AM Matthew House <[email protected]> wrote: > 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/CADBQv9YQFs5G%2BZiy4pFT7pSYZysbjDodUfY6tpe2HyyqaHp1Cg%40mail.gmail.com.
