On a question of Gino Giotto re df-cleq and ax-8

[Matthew House]

Recently, Gino Giotto posted a PR metamath/set.mm#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₀, v₁, v₂, …, 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 =₀, =₁, =₂, … acts solely on the values of its arguments and not the indices. To restate the definition, we have (x =_i y ↔ (x¹ = y¹ ∧ x² = i ∧ y² = 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₀ = v₁ → (v₀ ∈ z → v₁ ∈ z)) is invalidated by the assignment v₀ = v₁ = 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² = i from other possible values of x²; 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

[Matthew House]

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² = 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.

[Matthew House]

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 "v_i = v_j" have the usual meaning, and let "v_i ∈ v_j" be true iff v_i < v_j XOR v_i < 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 ∀v_i(v_i ∈ x ↔ v_i ∈ 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 v_i, 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 (ℚ\ℤ)ⁿ, 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.