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. On Tuesday, September 9, 2025 at 7:44:40 AM UTC-4 [email protected] wrote: > 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. > -- 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/718f834f-2f18-436e-a9e0-b6c313be92f6n%40googlegroups.com.
