Correction: the first line of the abidc proof should be |- ( x =s y -> ( y e.c A <-> x e.c A ) )
with a set equality on the left (since class equality is not yet introduced yet). We also want ax-8c to reference only primitive term constructors, so it should also use =s . On Mon, Nov 1, 2021 at 11:55 AM Mario Carneiro <[email protected]> wrote: > Regarding the new axioms: > > ax-abidc should be derivable from df-cleq (it should not be expressible > prior to this anyway, since A = B as a wff is not introduced until then). > Specifically: > > |- ( x = y -> ( y e.c A <-> x e.c A ) ) > |- ( y e.c A <-> [ y / x ] x e.c A ) > |- ( y e.c A <-> y e.c { x | x e.c A } ) > |- A. y ( y e.c A <-> y e.c { x | x e.c A } ) > |- A = { x | x e.c A } > > We need ax-8c as an axiom to prove the first line, but abidc should be > derivable. > > The second axiom, ( x e.c y <-> x e.s y ), is actually a definition: If > we indicate the coercion explicitly as ( x e.c cv y <-> x e.s y ), then > it should be clear that we can write it in definition form as > > |- cv y = { x | x e.s y } > > (which looks a lot like abidc but only because of the suggestive notation). > > On Mon, Nov 1, 2021 at 11:34 AM Thierry Arnoux <[email protected]> > wrote: > >> I was curious about the solution where we do not overload equality `=` >> and membership `e.`, but instead have different versions of those >> predicates for sets. >> >> For those interested, I've published the resulting experiment here: >> https://github.com/tirix/set-noov.mm >> >> One can examine the changes done on set.mm using GitHub's diff tool. >> I've also put a description of my changes in the README. >> >> In order to make that work, I had to introduce two new axioms. I wonder >> if anyone can eliminate any of them, or propose a cleverer approach. >> >> In any case, this approach involves duplicating many of the predicate >> calculus theorems, proving them once in their set-only version, and then >> again in their class version, so overall this method is not elegant and >> I agree it shall not be pursued. >> >> BR, >> _ >> Thierry >> >> >> On 29/10/2021 07:19, Norman Megill wrote: >> > On 10/28/21 10:11 AM, Thierry Arnoux wrote: >> > >> > > A solution is mentioned in the comment for df-cleq, shall it be >> > > reconsidered? >> > ... >> > >> > A discussion about eliminating overloading of = and e. in >> > df-clab,cleq,clel, and why it isn't that simple, is here (from 2016): >> > >> > https://groups.google.com/g/metamath/c/IwlpCJVPSLY/m/f8H9lze_BQAJ >> > >> > I believe Mario correctly concludes (contrary to my initial >> > suggestion) that overloading of "e." can't be removed with this >> > method. Since the 3 definitions work together, it doesn't make sense >> > to half-fix it with the clumsiness and longer proofs that will result >> > from =_2 (always having to convert back and forth to make use of FOL >> > theorems). >> > >> > I have removed the comment you mention from df-cleq since it is >> > misleading in this way. >> >> >> >> >> -- >> 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 on the web visit >> https://groups.google.com/d/msgid/metamath/f387c42a-ac19-3979-851b-d5b6fb8e2638%40gmx.net >> . >> > -- 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 on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSutSTcXhDB_ucpWitfy3ej7TpMO8MHS%2B-0a7FVzy36TcQ%40mail.gmail.com.
