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/b806bb10-2dc1-4dd6-8fd8-e45ef9afdddan%40googlegroups.com.
