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.

[Gino Giotto]

The thing I find puzzling about df-cleq is that, even if we can't derive ax-8, we can still derive a few theorems in the primitive language that don't seem to be provable without it. A few examples:

${
  $d x v u t $.  $d y v u t $.
  cleqv $p |- ( A. x x e. t <-> A. y y e. t ) $=
    ( vu vv cv wcel wal weq cab wb equid vexw tbt albii dfcleq bitr3i bianir ex
    wceq pm5.1 expcom impbid ax-mp 3bitri ) AFZCFZGZAHUHUFDDIZEJZGZKZAHZBFZUGGZ
    UNUJGZKZBHZUOBHUHULAUKUHUIEADLZMNOUMUGUJTURAUGUJPBUGUJPQUQUOBUPUQUOKUIEBUSM
    UPUQUOUPUQUOUPUORSUOUPUQUOUPUAUBUCUDOUE $.
$}

MM> sh tr cleqv /ma ax-* /ax
Statement "cleqv" assumes the following axioms ($a statements):
  ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-ext

${
  $d x v u t $.  $d y v u t $.
  cleqnul $p |- ( E. x x e. t <-> E. y y e. t ) $=
    ( vv vu cv wcel wex wn weq wb equid tbt notbi wsb df-clab 3bitri wal bicomi
    bitri cab 2th notbii a1i sbievw bitr2i bibi2i exbii df-ex nbbn con2bii wceq
    albii dfcleq notbid ) AFZCFZGZAHURIZUPDDJZIZEUAZGZKZAHZBFZUQGZIZVFVBGZKZBHZ
    VGBHURVDAURURBBJZKUSVLIZKVDVLURBLZMURVLNVMVCUSVCVAEAOVMVAAEPVAVMEAVAVMKEAJU
    TVLUTVLDLVNUBZUCUDUEUFUGQUHVEVDIZARZIVJIZBRZIZVKVDAUIVQVSVQURVCKZARZVGVIKZB
    RZVSVPWAAWAVPVDWAURVCUJUKSUMWBUQVBULZWDWEWBAUQVBUNSBUQVBUNTWCVRBVJWCVGVIUJU
    KUMQUCVKVTVJBUISQVJVGBVJVHVMKZVGVIVMVHVIVAEBOVMVABEPVAVMEBEBJZUTVLUTVLKWGVO
    UDUOUETUGVGVGVLKWFVLVGVNMVGVLNUFTUHQ $.
$}

MM> sh tr cleqnul /ma ax-* /ax
Statement "cleqnul" assumes the following axioms ($a statements):
  ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-ext

${
  $d x u v $.  $d y u v $.  $d x t $.  $d y t $.
  cleqsn $p |- ( A. x ( x e. t -> x = u ) -> ( x = u -> ( x = y -> ( x e. t -> y e. t ) ) ) ) $=
    ( vv weq cv wcel wi wal ax7 ax12v2 wb wsb df-clab equsb3 bibi1i albii com13
    dfcleq wa albiim cab bitr2i wceq bitri 3bitr3i sylbb 19.21bi biimpd syl6com
    sylbir ex com34 com3l sylcom ) ABFZACFZAGZDGZHZURIAJZVABGZUTHZIZUQURBCFZVBV
    EIABCKVBURVFVEVBURVAVFVDVAURVBVFVDIZURVAURVAIAJZVBVGIVAACLVHVBVGVHVBUAURVAM
    ZAJZVGURVAAUBVJVFVDVJVFVDMZBVJUSECFZEUCZHZVAMZAJZVKBJZVIVOAURVNVAVNVLEANURV
    LAEOEACPUDQRVMUTUEVCVMHZVDMZBJVPVQBVMUTTAVMUTTVSVKBVRVFVDVRVLEBNVFVLBEOEBCP
    UFQRUGUHUIUJULUMUKSUNUOUPS $.
$}

MM> sh tr cleqsn /ma ax-* /ax
Statement "cleqsn" assumes the following axioms ($a statements):
  ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-12 ax-ext

The first theorem is derived using the universal class, the second using the empty set, and the third one using the singleton. The question now is: are these theorems provable by only using their corresponding axioms listed above? If they are not, that would be enough to show the non-conservativity of the current df-cleq, because we used it to derive statements in the primitive language that wouldn't be derivable without it. I believe we can show it using the same model used by Benoit in his paper. In his model the universal quantifier is interpreted as the "do nothing" operation and equality is interpreted as the always true relation. So, for example, in cleqsn the first two antecedents trivially evaluate to true and the consequent is identical to ax-8 which we know it can evaluate to false. Therefore we have a model where cleqsn is invalid and the axioms used by cleqsn are valid, proving the non-conservativity of df-cleq over the listed set of axioms. In practice, this "leaking" of df-cleq means that I could still use it to cheat ax-8 usage in a few statements of set.mm.

[Matthew House]

For your cleqv, cleqnul, and cleqsn, it should indeed suffice to take a model with a single element equal to itself, an instance ∈_i which is always true, and an instance ∈_j which is always false. (The single-element model is basically what Benoît is talking about, assuming we want ax-12 to hold.) In these "∈_i" models where ax-8 is false, the only thing constraining the behavior of each instance is ax-ext, but ax-ext is trivially true when all elements are equal.

In general, proving non-conservative statements from df-cleq involves finding statements with an antecedent implying ∀x(x ∈_i y ↔ φ) for some wff φ. For cleqv, we have φ := ⊤; for cleqnul, we have φ := ⊥; and for cleqsn, we have φ := "x = u", with one direction of the biconditional coming from ax-12.